Implements a module performing DPLL style SAT checking. More...

#include <SATModule.h>

Inheritance diagram for smtrat::SATModule< Settings >:

Collaboration diagram for smtrat::SATModule< Settings >:

[legend]

Data Structures
struct	Abstraction
	Stores all information regarding a Boolean abstraction of a constraint. More...

struct	ClauseInformation

struct	CNFInfos

struct	lemma_lt

struct	LiteralClauses

struct	UnorderedClauseLookup

struct	VarData
	Stores information about a Minisat variable. More...

struct	VarOrderLt

struct	WatcherDeleted
	[Minisat related code] More...

Public Types
typedef Settings	SettingsType

enum class	LemmaType : unsigned { NORMAL = 0 , PERMANENT = 1 }

Public Member Functions
	SATModule (const ModuleInput _formula, Conditionals &_foundAnswer, Manager const _manager=nullptr)
	Constructs a SATModule. More...

	~SATModule ()
	Destructs this SATModule. More...

bool	addCore (ModuleInput::const_iterator)
	The module has to take the given sub-formula of the received formula into account. More...

Answer	checkCore ()
	Checks the received formula for consistency. More...

void	removeCore (ModuleInput::const_iterator)
	Removes everything related to the given sub-formula of the received formula. More...

void	updateModel () const
	Updates the model, if the solver has detected the consistency of the received formula, beforehand. More...

void	updateAllModels ()
	Updates all satisfying models, if the solver has detected the consistency of the received formula, beforehand. More...

void	updateInfeasibleSubset ()
	Updates the infeasible subset found by the SATModule, if the received formula is unsatisfiable. More...

void	cleanUpAfterOptimizing (const std::vector< Minisat::CRef > &_excludedAssignments)

void	removeUpperBoundOnMinimal ()

void	addConstraintToInform (const FormulaT &)
	Adds a constraint to the collection of constraints of this module, which are informed to a freshly generated backend. More...

void	addConstraintToInform_ (const FormulaT &_formula)

void	addBooleanAssignments (RationalAssignment &_rationalAssignment) const
	Adds the Boolean assignments to the given assignments, which were determined by the Minisat procedure. More...

void	print (std::ostream &_out=std::cout, const std::string &_init="") const
	Prints everything. More...

void	printCurrentAssignment (std::ostream &=std::cout, const std::string &="") const
	Prints the current assignment of the SAT solver. More...

void	printConstraintLiteralMap (std::ostream &_out=std::cout, const std::string &_init="") const
	Prints the constraints to literal map. More...

void	printFormulaCNFInfosMap (std::ostream &_out=std::cout, const std::string &_init="") const
	Prints the formulas to clauses map. More...

void	printClauseInformation (std::ostream &_out=std::cout, const std::string &_init="") const
	Prints the clause information. More...

void	printBooleanVarMap (std::ostream &_out=std::cout, const std::string &_init="") const
	Prints map of the Boolean within the SAT solver to the given Booleans. More...

void	printBooleanConstraintMap (std::ostream &_out=std::cout, const std::string &_init="") const
	Prints the literal to constraint map. More...

void	printClause (Minisat::CRef _clause, bool _withAssignment=false, std::ostream &_out=std::cout, const std::string &_init="") const
	Prints the clause at the given reference. More...

void	printClause (const Minisat::vec< Minisat::Lit > &, bool _withAssignment=false, std::ostream &_out=std::cout, const std::string &_init="") const
	Prints the clause resulting from the given vector of literals. More...

void	printClauses (const Minisat::vec< Minisat::CRef > &_clauses, const std::string _name, std::ostream &_out=std::cout, const std::string &_init="", int=0, bool _withAssignment=false, bool _onlyNotSatisfied=false) const
	Prints all given clauses. More...

void	printDecisions (std::ostream &_out=std::cout, const std::string &_init="") const
	Prints the decisions the SAT solver has made. More...

void	printPropagatedLemmas (std::ostream &_out=std::cout, const std::string &_init="") const
	Prints the propagated lemmas for each variables which influence its value. More...

void	printLiteralsActiveOccurrences (std::ostream &_out=std::cout, const std::string &_init="") const
	Prints the literals' active occurrences in all clauses. More...

void	collectStats ()
	Collects the taken statistics. More...

bool	inform (const FormulaT &_constraint)
	Informs the module about the given constraint. More...

void	deinform (const FormulaT &_constraint)
	The inverse of informing about a constraint. More...

virtual void	init ()
	Informs all backends about the so far encountered constraints, which have not yet been communicated. More...

bool	add (ModuleInput::const_iterator _subformula)
	The module has to take the given sub-formula of the received formula into account. More...

virtual Answer	check (bool _final=false, bool _full=true, carl::Variable _objective=carl::Variable::NO_VARIABLE)
	Checks the received formula for consistency. More...

virtual void	remove (ModuleInput::const_iterator _subformula)
	Removes everything related to the given sub-formula of the received formula. More...

virtual std::list< std::vector< carl::Variable > >	getModelEqualities () const
	Partition the variables from the current model into equivalence classes according to their assigned value. More...

unsigned	currentlySatisfiedByBackend (const FormulaT &_formula) const

virtual unsigned	currentlySatisfied (const FormulaT &) const

bool	receivedVariable (carl::Variable::Arg _var) const

Answer	solverState () const

std::size_t	id () const

void	setId (std::size_t _id)
	Sets this modules unique ID to identify itself. More...

thread_priority	threadPriority () const

void	setThreadPriority (thread_priority _threadPriority)
	Sets the priority of this module to get a thread for running its check procedure. More...

const ModuleInput *	pReceivedFormula () const

const ModuleInput &	rReceivedFormula () const

const ModuleInput *	pPassedFormula () const

const ModuleInput &	rPassedFormula () const

const Model &	model () const

const std::vector< Model > &	allModels () const

const std::vector< FormulaSetT > &	infeasibleSubsets () const

const std::vector< Module * > &	usedBackends () const

const carl::FastSet< FormulaT > &	constraintsToInform () const

const carl::FastSet< FormulaT > &	informedConstraints () const

void	addLemma (const FormulaT &_lemma, const LemmaType &_lt=LemmaType::NORMAL, const FormulaT &_preferredFormula=FormulaT(carl::FormulaType::TRUE))
	Stores a lemma being a valid formula. More...

bool	hasLemmas ()
	Checks whether this module or any of its backends provides any lemmas. More...

void	clearLemmas ()
	Deletes all yet found lemmas. More...

const std::vector< Lemma > &	lemmas () const

ModuleInput::const_iterator	firstUncheckedReceivedSubformula () const

ModuleInput::const_iterator	firstSubformulaToPass () const

void	receivedFormulaChecked ()
	Notifies that the received formulas has been checked. More...

const smtrat::Conditionals &	answerFound () const

bool	isPreprocessor () const

virtual std::string	moduleName () const

carl::Variable	objective () const

bool	is_minimizing () const

void	excludeNotReceivedVariablesFromModel () const
	Excludes all variables from the current model, which do not occur in the received formula. More...

void	updateLemmas ()
	Stores all lemmas of any backend of this module in its own lemma vector. More...

void	collectTheoryPropagations ()

void	collectOrigins (const FormulaT &_formula, FormulasT &_origins) const
	Collects the formulas in the given formula, which are part of the received formula. More...

void	collectOrigins (const FormulaT &_formula, FormulaSetT &_origins) const

bool	hasValidInfeasibleSubset () const

void	checkInfSubsetForMinimality (std::vector< FormulaSetT >::const_iterator _infsubset, const std::string &_filename="smaller_muses", unsigned _maxSizeDifference=1) const
	Checks the given infeasible subset for minimality by storing all subsets of it, which have a smaller size which differs from the size of the infeasible subset not more than the given threshold. More...

virtual std::pair< bool, FormulaT >	getReceivedFormulaSimplified ()

void	print (const std::string &_initiation="***") const
	Prints everything relevant of the solver. More...

void	printReceivedFormula (const std::string &_initiation="***") const
	Prints the vector of the received formula. More...

void	printPassedFormula (const std::string &_initiation="***") const
	Prints the vector of passed formula. More...

void	printInfeasibleSubsets (const std::string &_initiation="***") const
	Prints the infeasible subsets. More...

void	printModel (std::ostream &_out=std::cout) const
	Prints the assignment of this module satisfying its received formula if it satisfiable and this module could find an assignment. More...

void	printAllModels (std::ostream &_out=std::cout)
	Prints all assignments of this module satisfying its received formula if it satisfiable and this module could find an assignment. More...

Static Public Member Functions
static void	freeSplittingVariable (const FormulaT &_splittingVariable)

Static Public Attributes
static size_t	mNumOfBranchVarsToStore = 5
	The number of different variables to consider for a probable infinite loop of branchings. More...

static std::vector< Branching >	mLastBranches = std::vector<Branching>(mNumOfBranchVarsToStore, Branching(typename Poly::PolyType(), 0))
	Stores the last branches in a cycle buffer. More...

static size_t	mFirstPosInLastBranches = 0
	The beginning of the cyclic buffer storing the last branches. More...

static std::vector< FormulaT >	mOldSplittingVariables
	Reusable splitting variables. More...

Protected Member Functions
virtual bool	informCore ([[maybe_unused]] const FormulaT &_constraint)
	Informs the module about the given constraint. More...

virtual void	deinformCore ([[maybe_unused]] const FormulaT &_constraint)
	The inverse of informing about a constraint. More...

virtual bool	addCore ([[maybe_unused]] ModuleInput::const_iterator formula)
	The module has to take the given sub-formula of the received formula into account. More...

virtual void	removeCore ([[maybe_unused]] ModuleInput::const_iterator formula)
	Removes everything related to the given sub-formula of the received formula. More...

bool	anAnswerFound () const
	Checks for all antecedent modules and those which run in parallel with the same antecedent modules, whether one of them has determined a result. More...

void	clearModel () const
	Clears the assignment, if any was found. More...

void	clearModels () const
	Clears all assignments, if any was found. More...

void	cleanModel () const
	Substitutes variable occurrences by its model value in the model values of other variables. More...

ModuleInput::iterator	passedFormulaBegin ()

ModuleInput::iterator	passedFormulaEnd ()

void	addOrigin (ModuleInput::iterator _formula, const FormulaT &_origin)
	Adds the given set of formulas in the received formula to the origins of the given passed formula. More...

const FormulaT &	getOrigins (ModuleInput::const_iterator _formula) const
	Gets the origins of the passed formula at the given position. More...

void	getOrigins (const FormulaT &_formula, FormulasT &_origins) const

void	getOrigins (const FormulaT &_formula, FormulaSetT &_origins) const

std::pair< ModuleInput::iterator, bool >	removeOrigin (ModuleInput::iterator _formula, const FormulaT &_origin)

std::pair< ModuleInput::iterator, bool >	removeOrigins (ModuleInput::iterator _formula, const std::shared_ptr< std::vector< FormulaT >> &_origins)

void	informBackends (const FormulaT &_constraint)
	Informs all backends of this module about the given constraint. More...

std::pair< ModuleInput::iterator, bool >	addReceivedSubformulaToPassedFormula (ModuleInput::const_iterator _subformula)
	Copies the given sub-formula of the received formula to the passed formula. More...

bool	originInReceivedFormula (const FormulaT &_origin) const

std::pair< ModuleInput::iterator, bool >	addSubformulaToPassedFormula (const FormulaT &_formula)
	Adds the given formula to the passed formula with no origin. More...

std::pair< ModuleInput::iterator, bool >	addSubformulaToPassedFormula (const FormulaT &_formula, const std::shared_ptr< std::vector< FormulaT >> &_origins)
	Adds the given formula to the passed formula. More...

std::pair< ModuleInput::iterator, bool >	addSubformulaToPassedFormula (const FormulaT &_formula, const FormulaT &_origin)
	Adds the given formula to the passed formula. More...

void	generateTrivialInfeasibleSubset ()
	Stores the trivial infeasible subset being the set of received formulas. More...

void	receivedFormulasAsInfeasibleSubset (ModuleInput::const_iterator _subformula)
	Stores an infeasible subset consisting only of the given received formula. More...

std::vector< FormulaT >::const_iterator	findBestOrigin (const std::vector< FormulaT > &_origins) const

void	getInfeasibleSubsets ()
	Copies the infeasible subsets of the passed formula. More...

std::vector< FormulaSetT >	getInfeasibleSubsets (const Module &_backend) const
	Get the infeasible subsets the given backend provides. More...

const Model &	backendsModel () const
	Stores the model of a backend which determined satisfiability of the passed formula in the model of this module. More...

void	getBackendsModel () const

void	getBackendsAllModels () const
	Stores all models of a backend in the list of all models of this module. More...

virtual Answer	runBackends (bool _final, bool _full, carl::Variable _objective)
	Runs the backend solvers on the passed formula. More...

virtual Answer	runBackends ()

virtual ModuleInput::iterator	eraseSubformulaFromPassedFormula (ModuleInput::iterator _subformula, bool _ignoreOrigins=false)
	Removes everything related to the sub-formula to remove from the passed formula in the backends of this module. More...

void	clearPassedFormula ()

std::vector< FormulaT >	merge (const std::vector< FormulaT > &, const std::vector< FormulaT > &) const
	Merges the two vectors of sets into the first one. More...

size_t	determine_smallest_origin (const std::vector< FormulaT > &origins) const

bool	probablyLooping (const typename Poly::PolyType &_branchingPolynomial, const Rational &_branchingValue) const
	Checks whether given the current branching value and branching variable/polynomial it is (highly) probable that this branching is part of an infinite loop of branchings. More...

bool	branchAt (const Poly &_polynomial, bool _integral, const Rational &_value, std::vector< FormulaT > &&_premise, bool _leftCaseWeak=true, bool _preferLeftCase=true, bool _useReceivedFormulaAsPremise=false)
	Adds a lemmas which provoke a branching for the given variable at the given value, if this module returns Unknown and there exists a preceding SATModule. More...

bool	branchAt (const Poly &_polynomial, bool _integral, const Rational &_value, bool _leftCaseWeak=true, bool _preferLeftCase=true, bool _useReceivedFormulaAsPremise=false, const std::vector< FormulaT > &_premise=std::vector< FormulaT >())

bool	branchAt (carl::Variable::Arg _var, const Rational &_value, std::vector< FormulaT > &&_premise, bool _leftCaseWeak=true, bool _preferLeftCase=true, bool _useReceivedFormulaAsPremise=false)

bool	branchAt (carl::Variable::Arg _var, const Rational &_value, bool _leftCaseWeak=true, bool _preferLeftCase=true, bool _useReceivedFormulaAsPremise=false, const std::vector< FormulaT > &_premise=std::vector< FormulaT >())

void	splitUnequalConstraint (const FormulaT &)
	Adds the following lemmas for the given constraint p!=0. More...

unsigned	checkModel () const

void	addInformationRelevantFormula (const FormulaT &formula)
	Adds a formula to the InformationRelevantFormula. More...

const std::set< FormulaT > &	getInformationRelevantFormulas ()
	Gets all InformationRelevantFormulas. More...

bool	isLemmaLevel (LemmaLevel level)
	Checks if current lemma level is greater or equal to given level. More...

Static Protected Member Functions
static bool	modelsDisjoint (const Model &_modelA, const Model &_modelB)
	Checks whether there is no variable assigned by both models. More...

Protected Attributes
std::vector< FormulaSetT >	mInfeasibleSubsets
	Stores the infeasible subsets. More...

Manager *const	mpManager
	A reference to the manager. More...

Model	mModel
	Stores the assignment of the current satisfiable result, if existent. More...

std::vector< Model >	mAllModels
	Stores all satisfying assignments. More...

bool	mModelComputed
	True, if the model has already been computed. More...

bool	mFinalCheck
	true, if the check procedure should perform a final check which especially means not to postpone splitting decisions More...

bool	mFullCheck
	false, if this module should avoid too expensive procedures and rather return unknown instead. More...

carl::Variable	mObjectiveVariable
	Objective variable to be minimized. If set to NO_VARIABLE, a normal sat check should be performed. More...

std::vector< TheoryPropagation >	mTheoryPropagations

std::atomic< Answer >	mSolverState
	States whether the received formula is known to be satisfiable or unsatisfiable otherwise it is set to unknown. More...

std::atomic_bool *	mBackendsFoundAnswer
	This flag is passed to any backend and if it determines an answer to a prior check call, this flag is fired. More...

Conditionals	mFoundAnswer
	Vector of Booleans: If any of them is true, we have to terminate a running check procedure. More...

std::vector< Module * >	mUsedBackends
	The backends of this module which are currently used (conditions to use this module are fulfilled for the passed formula). More...

std::vector< Module * >	mAllBackends
	The backends of this module which have been used. More...

ModuleInput::iterator	mFirstSubformulaToPass
	Stores the position of the first sub-formula in the passed formula, which has not yet been considered for a consistency check of the backends. More...

carl::FastSet< FormulaT >	mConstraintsToInform
	Stores the constraints which the backends must be informed about. More...

carl::FastSet< FormulaT >	mInformedConstraints
	Stores the position of the first constraint of which no backend has been informed about. More...

ModuleInput::const_iterator	mFirstUncheckedReceivedSubformula
	Stores the position of the first (by this module) unchecked sub-formula of the received formula. More...

unsigned	mSmallerMusesCheckCounter
	Counter used for the generation of the smt2 files to check for smaller muses. More...

std::vector< std::size_t >	mVariableCounters
	Maps variables to the number of their occurrences. More...

Private Types
using	VarScheduler = typename Settings::VarScheduler

typedef carl::FastMap< FormulaT, std::vector< Minisat::Lit > >	ConstraintLiteralsMap
	Maps the constraints occurring in the SAT module to their abstractions. More...

typedef carl::FastMap< carl::Variable, Minisat::Var >	BooleanVarMap
	Maps the Boolean variables to their corresponding Minisat variable. More...

typedef std::unordered_map< int, FormulaT >	MinisatVarMap
	Maps the Minisat variables to their corresponding boolean variable. More...

typedef Minisat::vec< std::pair< Abstraction , Abstraction > >	BooleanConstraintMap
	Maps each Minisat variable to a pair of Abstractions, one contains the abstraction information of the literal being the variable and one contains the abstraction information of the literal being the variables negation. More...

typedef carl::FastMap< FormulaT, CNFInfos >	FormulaCNFInfosMap
	Maps the clauses in the received formula to the corresponding Minisat clause. More...

typedef std::map< Minisat::Var, FormulasT >	VarLemmaMap
	Maps the minisat variable to the formulas which influence its value. More...

typedef std::vector< std::vector< Minisat::Lit > >	ClauseVector
	A vector of vectors of literals representing a vector of clauses. More...

typedef std::set< std::vector< int > >	ClauseSet
	A set of vectors of integer representing a set of clauses. More...

typedef carl::FastMap< signed, std::vector< signed > >	TseitinVarShadows

Private Member Functions
Minisat::Var	newVar (bool polarity=true, bool dvar=true, double _activity=0, bool insertIntoHeap=true)
	Creates a new SAT variable in the solver. More...

void	simplify ()
	Removes already satisfied clauses and performs simplifications on all clauses. More...

bool	addClause (const Minisat::vec< Minisat::Lit > &_clause, unsigned _type=0)
	Adds the clause of the given type with the given literals to the clauses managed by Minisat. More...

void	removeLiteralOrigin (Minisat::Lit _litToRemove, const FormulaT &_origin)

bool	okay () const

void	setPolarity (Minisat::Var v, bool b)
	Declare which polarity the decision heuristic should use for a variable. More...

void	setDecisionVar (Minisat::Var v, bool b, bool insertIntoHeap=true)
	Declare if a variable should be eligible for selection in the decision heuristic. More...

Minisat::lbool	bool_value (Minisat::Var x) const

Minisat::lbool	value (Minisat::Var x) const

Minisat::lbool	theoryValue (Minisat::Var x) const

bool	addClauseIfNew (const FormulasT &clause)

void	handleTheoryConflict (const mcsat::Explanation &explanation)

Minisat::lbool	bool_value (Minisat::Lit p) const

Minisat::lbool	value (Minisat::Lit p) const

Minisat::lbool	theoryValue (Minisat::Lit p) const

int	nAssigns () const

int	nClauses () const

int	nLearnts () const

int	nVars () const

int	nFreeVars () const

void	setConfBudget (int64_t x)
	[Minisat related code] More...

void	setPropBudget (int64_t x)
	[Minisat related code] More...

void	budgetOff ()
	[Minisat related code] More...

void	interrupt ()
	Trigger a (potentially asynchronous) interruption of the solver. More...

void	clearInterrupt ()
	Clear interrupt indicator flag. More...

void	garbageCollect ()
	[Minisat related code] More...

void	checkGarbage (double gf)
	[Minisat related code] More...

void	checkGarbage (void)
	[Minisat related code] More...

void	printSatState (std::ostream &=std::cout, const std::string="")
	[Minisat related code] More...

void	insertVarOrder (Minisat::Var x)
	Insert a variable in the decision order priority queue. More...

void	decrementLearntSizeAdjustCnt ()
	[Minisat related code] More...

bool	fullAssignment ()

Minisat::Lit	pickBranchLit ()

void	checkAbstractionsConsistency ()

void	newDecisionLevel ()
	Begins a new decision level. More...

void	decrementTseitinShadowOccurrences (signed _var)

void	incrementTseitinShadowOccurrences (signed _var)

void	uncheckedEnqueue (Minisat::Lit p, Minisat::CRef from=Minisat::CRef_Undef)
	Enqueue a literal. More...

bool	enqueue (Minisat::Lit p, Minisat::CRef from=Minisat::CRef_Undef)
	Test if fact 'p' contradicts current state, enqueue otherwise. More...

Minisat::CRef	propagate ()
	propagate : [void] -> [Clause*] More...

void	cancelUntil (int level, bool force=false)
	Revert to the state at given level (keeping all assignments at 'level' but not beyond). More...

void	cancelIncludingLiteral (Minisat::Lit lit)

void	cancelAssignmentUntil (int level)
	Revert the variables assignment until a given level (keeping all assignments at 'level') More...

void	resetVariableAssignment (Minisat::Var _var)

bool	analyze (Minisat::CRef confl, Minisat::vec< Minisat::Lit > &out_learnt, int &out_btlevel)
	analyze : (confl : Clause*) (out_learnt : vec<Lit>&) (out_btlevel : int&) -> [void] More...

bool	litRedundant (Minisat::Lit p, uint32_t abstract_levels)
	Check if 'p' can be removed. More...

bool	processLemmas ()
	Adds clauses representing the lemmas which should be added to this SATModule. More...

void	learnTheoryConflicts ()
	Adds the clauses representing all conflicts generated by all backends. More...

void	adaptConflictEvaluation (size_t &_clauseEvaluation, Minisat::Lit _lit, bool _firstLiteral)

Minisat::CRef	propagateConsistently (bool _checkWithTheory=true)
	Propagate and check the consistency of the constraints, whose abstraction literals have been assigned to true. More...

void	propagateTheory ()

void	theoryCall ()

void	constructLemmas ()

bool	expPositionsCorrect () const

Minisat::lbool	checkFormula ()
	Checks the received formula for consistency. More...

void	computeAdvancedLemmas ()

Minisat::lbool	search (int nof_conflicts=100)
	search : (nof_conflicts : int) (params : const SearchParams&) -> [lbool] More...

void	handleConflict (Minisat::CRef _confl)
	Handles conflict. More...

void	reduceDB ()
	reduceDB : () -> [void] More...

void	clearLearnts (int n)

void	removeSatisfied (Minisat::vec< Minisat::CRef > &cs)
	Removes all satisfied clauses from the given vector of clauses, which should only be performed in decision level 0. More...

void	rebuildOrderHeap ()
	[Minisat related code] More...

double	maxActivity () const

void	varDecayActivity ()
	Decay all variables with the specified factor. More...

void	varBumpActivity (Minisat::Var v, double inc)
	Increase a variable with the current 'bump' value. More...

void	varBumpActivity (Minisat::Var v)
	Increase a variable with the current 'bump' value. More...

void	claDecayActivity ()
	Decay all clauses with the specified factor. More...

void	claBumpActivity (Minisat::Clause &c)
	Increase a clause with the current 'bump' value. More...

void	attachClause (Minisat::CRef cr)
	Attach a clause to watcher lists. More...

void	detachClause (Minisat::CRef cr, bool strict=false)
	Detach a clause to watcher lists. More...

void	removeClause (Minisat::CRef cr)
	Detach and free a clause. More...

Minisat::Clause &	getClause (Minisat::CRef cr)

bool	locked (const Minisat::Clause &c)

bool	satisfied (const Minisat::Clause &c) const

bool	bool_satisfied (const Minisat::Clause &c) const

void	relocAll (Minisat::ClauseAllocator &to)
	[Minisat related code] More...

int	decisionLevel () const

uint32_t	abstractLevel (Minisat::Var x) const
	Used to represent an abstraction of sets of decision levels. More...

Minisat::CRef	reason (Minisat::Var x)

void	removeTheoryPropagation (int _position)

int	level (Minisat::Var x) const

int	theory_level (Minisat::Var x) const

int	min_theory_level (Minisat::Var x) const

int	trailIndex (Minisat::Var _var) const

int	level (const Minisat::vec< Minisat::Lit > &) const

Minisat::CRef	storeLemmas ()

double	progressEstimate () const

bool	withinBudget () const

void	updateCNFInfoCounter (typename FormulaCNFInfosMap::iterator _iter, const FormulaT &_origin, bool _increment)

void	addClause_ (const Minisat::vec< Minisat::Lit > &_clause, unsigned _type, const FormulaT &_original, typename FormulaCNFInfosMap::iterator _formulaCNFInfoIter)

Minisat::Lit	addClauses (const FormulaT &_formula, unsigned _type, unsigned _depth=0, const FormulaT &_original=FormulaT(carl::FormulaType::TRUE))

void	addXorClauses (const Minisat::vec< Minisat::Lit > &_literals, const Minisat::vec< Minisat::Lit > &_negLiterals, int _from, bool _numOfNegatedLitsEven, unsigned _type, Minisat::vec< Minisat::Lit > &_clause, const FormulaT &_original, typename FormulaCNFInfosMap::iterator _formulaCNFInfoIter)

bool	supportedConstraintType (const FormulaT &_formula) const

Minisat::Lit	createLiteral (const FormulaT &_formula, const FormulaT &_origin=FormulaT(carl::FormulaType::TRUE), bool _decisionRelevant=true)
	Creates or simply returns the literal belonging to the formula being the first argument. More...

Minisat::Lit	getLiteral (const FormulaT &_formula) const

void	adaptPassedFormula ()
	Adapts the passed formula according to the current assignment within the SAT solver. More...

void	adaptPassedFormula (Abstraction &_abstr)
	Adapts the passed formula according to the given abstraction information. More...

bool	passedFormulaCorrect () const

void	updateModel (Model &model, bool only_relevant_variables=false) const
	Updates the model, if the solver has detected the consistency of the received formula, beforehand. More...

std::pair< ModuleInput::iterator, bool >	addSubformulaToPassedFormula (const FormulaT &_formula, bool _hasSingleOrigin, const FormulaT &_origin, const std::shared_ptr< std::vector< FormulaT >> &_origins, bool _mightBeConjunction)
	This method actually implements the adding of a formula to the passed formula. More...

Answer	foundAnswer (Answer _answer)
	Sets the solver state to the given answer value. More...

Static Private Member Functions
static Minisat::Var	mapVar (Minisat::Var x, Minisat::vec< Minisat::Var > &map, Minisat::Var &max)
	[Minisat related code] More...

static double	luby (double y, int x)
	Finite subsequences of the Luby-sequence: More...

static double	drand (double &seed)

static int	irand (double &seed, int size)

Private Attributes
int	verbosity
	[Minisat related code] More...

double	var_decay
	[Minisat related code] More...

double	clause_decay
	[Minisat related code] More...

double	random_var_freq
	[Minisat related code] More...

double	random_seed
	[Minisat related code] More...

bool	luby_restart
	[Minisat related code] More...

int	ccmin_mode
	Controls conflict clause minimization (0=none, 1=basic, 2=deep). More...

int	phase_saving
	Controls the level of phase saving (0=none, 1=limited, 2=full). More...

bool	rnd_pol
	Use random polarities for branching heuristics. More...

bool	rnd_init_act
	Initialize variable activities with a small random value. More...

double	garbage_frac
	The fraction of wasted memory allowed before a garbage collection is triggered. More...

int	restart_first
	The initial restart limit. (default 100) More...

double	restart_inc
	The factor with which the restart limit is multiplied in each restart. (default 1.5) More...

double	learntsize_factor
	The initial limit for learned clauses is a factor of the original clauses.(default 1 / 3) More...

double	learntsize_inc
	The limit for learned clauses is multiplied with this factor each restart.(default 1.1) More...

int	learntsize_adjust_start_confl
	[Minisat related code] More...

double	learntsize_adjust_inc
	[Minisat related code] More...

uint64_t	solves
	[Minisat related code] More...

uint64_t	starts

uint64_t	decisions

uint64_t	rnd_decisions

uint64_t	propagations

uint64_t	conflicts

uint64_t	dec_vars
	[Minisat related code] More...

uint64_t	clauses_literals

uint64_t	learnts_literals

uint64_t	max_literals

uint64_t	tot_literals

bool	ok
	If FALSE, the constraints are already unsatisfiable. No part of the solver state may be used! More...

Minisat::vec< Minisat::CRef >	clauses
	List of problem clauses. More...

Minisat::vec< Minisat::CRef >	satisfiedClauses
	List of problem clauses. More...

Minisat::vec< Minisat::CRef >	learnts
	List of learned clauses. More...

Minisat::vec< Minisat::CRef >	unknown_excludes
	List of clauses which exclude a call resulted in unknown. More...

double	cla_inc
	Amount to bump next clause with. More...

Minisat::vec< double >	activity
	A heuristic measurement of the activity of a variable. More...

double	var_inc
	Amount to bump next variable with. More...

Minisat::OccLists< Minisat::Lit, Minisat::vec< Minisat::Watcher >, WatcherDeleted >	watches
	'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true). More...

Minisat::vec< Minisat::lbool >	assigns
	The current assignments. More...

Minisat::vec< char >	polarity
	The preferred polarity of each variable. More...

Minisat::vec< char >	decision
	Declares if a variable is eligible for selection in the decision heuristic. More...

Minisat::vec< Minisat::Lit >	trail
	Assignment stack; stores all assignments made in the order they were made. More...

Minisat::vec< int >	trail_lim
	Separator indices for different decision levels in 'trail'. More...

Minisat::vec< VarData >	vardata
	Stores reason and level for each variable. More...

int	qhead
	Head of queue (as index into the trail – no more explicit propagation queue in MiniSat). More...

int	simpDB_assigns
	Number of top-level assignments since last execution of 'simplify()'. More...

int64_t	simpDB_props
	Remaining number of propagations that must be made before next execution of 'simplify()'. More...

Minisat::vec< Minisat::Lit >	assumptions
	Current set of assumptions provided to solve by the user. More...

VarScheduler	var_scheduler
	A priority queue of variables. More...

double	progress_estimate
	Set by 'search()'. More...

bool	remove_satisfied
	Indicates whether possibly inefficient linear scan for satisfied clauses should be performed in 'simplify'. More...

Minisat::ClauseAllocator	ca
	[Minisat related code] More...

Minisat::vec< char >	seen
	Each variable is prefixed by the method in which it is used, except 'seen' which is used in several places. More...

Minisat::vec< Minisat::Lit >	analyze_stack
	[Minisat related code] More...

Minisat::vec< Minisat::Lit >	analyze_toclear
	[Minisat related code] More...

Minisat::vec< Minisat::Lit >	add_tmp
	[Minisat related code] More...

double	max_learnts
	[Minisat related code] More...

double	learntsize_adjust_confl
	[Minisat related code] More...

int	learntsize_adjust_cnt
	[Minisat related code] More...

int64_t	conflict_budget
	-1 means no budget. More...

int64_t	propagation_budget
	-1 means no budget. More...

bool	asynch_interrupt
	[Minisat related code] More...

Minisat::vec< Minisat::Lit >	learnt_clause
	For temporary usage. More...

Minisat::Var	mTrueVar
	Variable representing true. More...

bool	mChangedPassedFormula
	A flag, which is set to true, if anything has been changed in the passed formula between now and the last consistency check. More...

bool	mComputeAllSAT
	A flag, which is set to true, if all satisfying assignments should be computed. More...

bool	mFullAssignmentCheckedForConsistency

bool	mOptimumComputed

bool	mBusy

bool	mExcludedAssignments

Answer	mCurrentAssignmentConsistent
	Stores gained information about the current assignment's consistency. More...

size_t	mNumberOfFullLazyCalls
	The number of full laze calls made. More...

int	mCurr_Restarts
	The number of restarts made. More...

unsigned	mNumberOfTheoryCalls
	The number of theory calls made. More...

bool	mReceivedFormulaPurelyPropositional

BooleanConstraintMap	mBooleanConstraintMap
	Maps each Minisat variable to a pair of Abstractions, one contains the abstraction information of the literal being the variable and one contains the abstraction information of the literal being the variables negation. More...

ConstraintLiteralsMap	mConstraintLiteralMap
	Maps the constraints occurring in the SAT module to their abstractions. More...

BooleanVarMap	mBooleanVarMap
	Maps the Boolean variables to their corresponding Minisat variable. More...

MinisatVarMap	mMinisatVarMap
	Maps the Minisat variables to their corresponding boolean variable. More...

carl::FastMap< FormulaT, Minisat::Lit >	mFormulaAssumptionMap

FormulaCNFInfosMap	mFormulaCNFInfosMap
	Maps the clauses in the received formula to the corresponding Minisat clause and Minisat literal. More...

ClauseSet	mLearntDeductions
	If problem is unsatisfiable (possibly under assumptions), this vector represent the final conflict clause expressed in the assumptions. More...

carl::FastMap< Minisat::CRef, ClauseInformation >	mClauseInformation

std::unordered_map< int, std::unordered_set< Minisat::CRef > >	mLiteralClausesMap

size_t	mNumberOfSatisfiedClauses

std::vector< signed >	mChangedBooleans
	Stores all Literals for which the abstraction information might be changed. More...

bool	mAllActivitiesChanged
	Is true, if we have to communicate all activities to the backends. (This might be the case after rescaling the activities.) More...

std::vector< signed >	mChangedActivities
	Stores all clauses in which the activities have been changed. More...

VarLemmaMap	mPropagatedLemmas
	Stores for each variable the corresponding formulas which control its value. More...

std::vector< int >	mRelevantVariables
	Stores Minisat indexes of all relevant variables. More...

Minisat::vec< unsigned >	mNonTseitinShadowedOccurrences

TseitinVarShadows	mTseitinVarShadows

carl::FastMap< int, FormulaT >	mTseitinVarFormulaMap

carl::Bitset	mTseitinVariable
	Stores whether a given variable is a tseitin variable. More...

carl::Bitset	mAssumedTseitinVariable
	Stores whether a given tseitin variable was already added to the assumptions. More...

carl::Bitset	mNonassumedTseitinVariable
	Stores whether a given tseitin variable was not yet added to the assumptions, but represents a top-level clause. More...

std::vector< Minisat::vec< Minisat::Lit > >	mCurrentTheoryConflicts

std::vector< unsigned >	mCurrentTheoryConflictTypes

std::map< std::pair< size_t, size_t >, size_t >	mCurrentTheoryConflictEvaluations

std::unordered_set< int >	mLevelCounter

size_t	mTheoryConflictIdCounter

ModuleInput::iterator	mUpperBoundOnMinimal

std::vector< LiteralClauses >	mLiteralsClausesMap

std::vector< std::pair< size_t, size_t > >	mLiteralsActivOccurrences

std::vector< Minisat::Lit >	mPropagationFreeDecisions

Minisat::vec< Minisat::vec< Minisat::Lit > >	mLemmas
	literals propagated by lemmas More...

Minisat::vec< bool >	mLemmasRemovable
	is the lemma removable More...

mcsat::MCSATMixin< typename Settings::MCSATSettings >	mMCSAT

std::map< carl::Variable, std::vector< signed > >	mFutureChangedBooleans

UnorderedClauseLookup	mUnorderedClauseLookup

friend	Manager

std::size_t	mId
	A unique ID to identify this module instance. (Could be useful but currently nowhere used) More...

thread_priority	mThreadPriority
	The priority of this module to get a thread for running its check procedure. More...

const ModuleInput *	mpReceivedFormula
	The formula passed to this module. More...

ModuleInput *	mpPassedFormula
	The formula passed to the backends of this module. More...

std::string	mModuleName

ModuleStatistics &	mStatistics = statistics_get<ModuleStatistics>(moduleName())

Friends
class	VarSchedulerBase

class	VarSchedulerMcsatBase

Detailed Description

template<class Settings>
class smtrat::SATModule< Settings >

Implements a module performing DPLL style SAT checking.

It is mainly based on Minisat 2.0 and extends it by enabling the SMT-RAT module interfaces and some optimizations.

Definition at line 60 of file SATModule.h.

Member Typedef Documentation

◆ BooleanConstraintMap

template<class Settings >

typedef Minisat::vec<std::pair<Abstraction*,Abstraction*> > smtrat::SATModule< Settings >::BooleanConstraintMap

private

Maps each Minisat variable to a pair of Abstractions, one contains the abstraction information of the literal being the variable and one contains the abstraction information of the literal being the variables negation.

Definition at line 320 of file SATModule.h.

◆ BooleanVarMap

template<class Settings >

typedef carl::FastMap<carl::Variable, Minisat::Var> smtrat::SATModule< Settings >::BooleanVarMap

private

Maps the Boolean variables to their corresponding Minisat variable.

Definition at line 311 of file SATModule.h.

◆ ClauseSet

template<class Settings >

typedef std::set<std::vector<int> > smtrat::SATModule< Settings >::ClauseSet

private

A set of vectors of integer representing a set of clauses.

Definition at line 332 of file SATModule.h.

◆ ClauseVector

template<class Settings >

typedef std::vector<std::vector<Minisat::Lit> > smtrat::SATModule< Settings >::ClauseVector

private

A vector of vectors of literals representing a vector of clauses.

Definition at line 329 of file SATModule.h.

◆ ConstraintLiteralsMap

template<class Settings >

typedef carl::FastMap<FormulaT, std::vector<Minisat::Lit> > smtrat::SATModule< Settings >::ConstraintLiteralsMap

private

Maps the constraints occurring in the SAT module to their abstractions.

We store a vector of literals for each constraints, which is only used in the optimization, which applies valid substitutions.

Definition at line 308 of file SATModule.h.

◆ FormulaCNFInfosMap

template<class Settings >

typedef carl::FastMap<FormulaT, CNFInfos> smtrat::SATModule< Settings >::FormulaCNFInfosMap

private

Maps the clauses in the received formula to the corresponding Minisat clause.

Definition at line 323 of file SATModule.h.

◆ MinisatVarMap

template<class Settings >

typedef std::unordered_map<int,FormulaT> smtrat::SATModule< Settings >::MinisatVarMap

private

Maps the Minisat variables to their corresponding boolean variable.

Definition at line 314 of file SATModule.h.

◆ SettingsType

template<class Settings >

typedef Settings smtrat::SATModule< Settings >::SettingsType

Definition at line 673 of file SATModule.h.

◆ TseitinVarShadows

template<class Settings >

typedef carl::FastMap<signed,std::vector<signed> > smtrat::SATModule< Settings >::TseitinVarShadows

private

Definition at line 335 of file SATModule.h.

◆ VarLemmaMap

template<class Settings >

typedef std::map<Minisat::Var, FormulasT> smtrat::SATModule< Settings >::VarLemmaMap

private

Maps the minisat variable to the formulas which influence its value.

Definition at line 326 of file SATModule.h.

◆ VarScheduler

template<class Settings >

using smtrat::SATModule< Settings >::VarScheduler = typename Settings::VarScheduler

private

Definition at line 218 of file SATModule.h.

Member Enumeration Documentation

◆ LemmaType

enum smtrat::Module::LemmaType : unsigned

stronginherited

Enumerator
NORMAL
PERMANENT

Definition at line 123 of file Module.h.

Constructor & Destructor Documentation

◆ SATModule()

template<class Settings >

smtrat::SATModule< Settings >::SATModule	(	const ModuleInput *	_formula,
		Conditionals &	_foundAnswer,
		Manager *const	_manager = `nullptr`
	)

Constructs a SATModule.

Parameters

_type	The type of this module being SATModule.
_formula	The formula passed to this module, called received formula.
_settings	[Not yet used.]
_foundAnswer	Vector of Booleans: If any of them is true, we have to terminate a running check procedure.
_manager	A reference to the manager of the solver using this module.

◆ ~SATModule()

template<class Settings >

smtrat::SATModule< Settings >::~SATModule ( )

Destructs this SATModule.

Member Function Documentation

◆ abstractLevel()

template<class Settings >

uint32_t smtrat::SATModule< Settings >::abstractLevel ( Minisat::Var x ) const

inlineprivate

Used to represent an abstraction of sets of decision levels.

Parameters

x	[Minisat related code]

Returns: [Minisat related code]

Definition at line 1592 of file SATModule.h.

Here is the call graph for this function:

◆ adaptConflictEvaluation()

template<class Settings >

void smtrat::SATModule< Settings >::adaptConflictEvaluation	(	size_t &	_clauseEvaluation,
		Minisat::Lit	_lit,
		bool	_firstLiteral
	)

private

◆ adaptPassedFormula() [1/2]

template<class Settings >

void smtrat::SATModule< Settings >::adaptPassedFormula ( )

private

Adapts the passed formula according to the current assignment within the SAT solver.

Returns: true, if the passed formula has been changed; false, otherwise.

◆ adaptPassedFormula() [2/2]

template<class Settings >

void smtrat::SATModule< Settings >::adaptPassedFormula ( Abstraction & _abstr )

private

Adapts the passed formula according to the given abstraction information.

Parameters

_abstr The information of a Boolean abstraction of a constraint (contains no information, if the Boolean does not correspond to a constraint's abstraction).

◆ add()

bool smtrat::Module::add ( ModuleInput::const_iterator _subformula )

inherited

The module has to take the given sub-formula of the received formula into account.

Parameters

_subformula The sub-formula to take additionally into account.

Returns: false, if it can be easily decided that this sub-formula causes a conflict with the already considered sub-formulas; true, otherwise.

Definition at line 138 of file Module.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ addBooleanAssignments()

template<class Settings >

void smtrat::SATModule< Settings >::addBooleanAssignments ( RationalAssignment & _rationalAssignment ) const

Adds the Boolean assignments to the given assignments, which were determined by the Minisat procedure.

Note: Assignments in the given map are not overwritten.

Parameters

_rationalAssignment The assignments to add the Boolean assignments to.

◆ addClause()

template<class Settings >

bool smtrat::SATModule< Settings >::addClause	(	const Minisat::vec< Minisat::Lit > &	_clause,
		unsigned	_type = `0`
	)

private

Adds the clause of the given type with the given literals to the clauses managed by Minisat.

Parameters

_clause	The clause to add.
_type	The type of the clause (NORMAL_CLAUSE, LEMMA_CLAUSE or CONFLICT_CLAUSE).
_force	If true backtracking won't stop at the first assumption-decision-level.

Returns: true, if a clause has been added; false, otherwise.

Here is the caller graph for this function:

◆ addClause_()

template<class Settings >

void smtrat::SATModule< Settings >::addClause_	(	const Minisat::vec< Minisat::Lit > &	_clause,
		unsigned	_type,
		const FormulaT &	_original,
		typename FormulaCNFInfosMap::iterator	_formulaCNFInfoIter
	)

inlineprivate

Definition at line 1687 of file SATModule.h.

Here is the call graph for this function:

◆ addClauseIfNew()

template<class Settings >

bool smtrat::SATModule< Settings >::addClauseIfNew ( const FormulasT & clause )

inlineprivate

Definition at line 961 of file SATModule.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ addClauses()

template<class Settings >

Minisat::Lit smtrat::SATModule< Settings >::addClauses	(	const FormulaT &	_formula,
		unsigned	_type,
		unsigned	_depth = `0`,
		const FormulaT &	_original = `FormulaT(carl::FormulaType::TRUE)`
	)

private

◆ addConstraintToInform()

template<class Settings >

void smtrat::SATModule< Settings >::addConstraintToInform ( const FormulaT & _constraint )

inlinevirtual

Adds a constraint to the collection of constraints of this module, which are informed to a freshly generated backend.

Parameters

_constraint The constraint to add.

Reimplemented from smtrat::Module.

Definition at line 734 of file SATModule.h.

◆ addConstraintToInform_()

template<class Settings >

void smtrat::SATModule< Settings >::addConstraintToInform_ ( const FormulaT & _formula )

inline

Definition at line 735 of file SATModule.h.

Here is the call graph for this function:

◆ addCore() [1/2]

virtual bool smtrat::Module::addCore ( [[maybe_unused] ] ModuleInput::const_iterator formula )

inlineprotectedvirtualinherited

The module has to take the given sub-formula of the received formula into account.

Parameters

formula The sub-formula to take additionally into account.

Returns: false, if it can be easily decided that this sub-formula causes a conflict with the already considered sub-formulas; true, otherwise.

Definition at line 706 of file Module.h.

Here is the caller graph for this function:

◆ addCore() [2/2]

template<class Settings >

bool smtrat::SATModule< Settings >::addCore ( ModuleInput::const_iterator )

The module has to take the given sub-formula of the received formula into account.

Parameters

_subformula The sub-formula to take additionally into account.

Returns: false, if it can be easily decided that this sub-formula causes a conflict with the already considered sub-formulas; true, otherwise.

◆ addInformationRelevantFormula()

void smtrat::Module::addInformationRelevantFormula ( const FormulaT & formula )

protectedinherited

Adds a formula to the InformationRelevantFormula.

Parameters

formula Formula to add

Definition at line 1068 of file Module.cpp.

Here is the call graph for this function:

◆ addLemma()

void smtrat::Module::addLemma	(	const FormulaT &	_lemma,
		const LemmaType &	_lt = `LemmaType::NORMAL`,
		const FormulaT &	_preferredFormula = `FormulaT( carl::FormulaType::TRUE )`
	)

inlineinherited

Stores a lemma being a valid formula.

Parameters

_lemma	The eduction/lemma to store.
_lt	The type of the lemma.
_preferredFormula	Hint for the next decision, which formula should be assigned to true.

Definition at line 521 of file Module.h.

Here is the call graph for this function:

◆ addOrigin()

void smtrat::Module::addOrigin	(	ModuleInput::iterator	_formula,
		const FormulaT &	_origin
	)

inlineprotectedinherited

Adds the given set of formulas in the received formula to the origins of the given passed formula.

Parameters

_formula	The passed formula to set the origins for.
_origin	A set of formulas in the received formula of this module.

Definition at line 798 of file Module.h.

Here is the call graph for this function:

◆ addReceivedSubformulaToPassedFormula()

std::pair<ModuleInput::iterator,bool> smtrat::Module::addReceivedSubformulaToPassedFormula ( ModuleInput::const_iterator _subformula )

inlineprotectedinherited

Copies the given sub-formula of the received formula to the passed formula.

Note, that there is always a link between sub-formulas of the passed formulas to sub-formulas of the received formulas, which are responsible for its occurrence.

Parameters

_subformula The sub-formula of the received formula to copy.

Definition at line 857 of file Module.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ addSubformulaToPassedFormula() [1/4]

std::pair<ModuleInput::iterator,bool> smtrat::Module::addSubformulaToPassedFormula ( const FormulaT & _formula )

inlineprotectedinherited

Adds the given formula to the passed formula with no origin.

Note that in the next call of this module's removeSubformula, all formulas in the passed formula without origins will be removed.

Parameters

_formula The formula to add to the passed formula.

Returns: A pair to the position where the formula to add has been inserted (or its first sub-formula which has not yet been in the passed formula, in case the formula to add is a conjunction), and a Boolean stating whether anything has been added to the passed formula.

Definition at line 873 of file Module.h.

Here is the caller graph for this function:

◆ addSubformulaToPassedFormula() [2/4]

std::pair< ModuleInput::iterator, bool > smtrat::Module::addSubformulaToPassedFormula	(	const FormulaT &	_formula,
		bool	_hasSingleOrigin,
		const FormulaT &	_origin,
		const std::shared_ptr< std::vector< FormulaT >> &	_origins,
		bool	_mightBeConjunction
	)

privateinherited

This method actually implements the adding of a formula to the passed formula.

Parameters

_formula	The formula to add to the passed formula.
_hasSingleOrigin	true, if the next argument contains the formula being the single origin.
_origin	The sub-formula of the received formula being responsible for the occurrence of the formula to add to the passed formula.
_origins	The link of the formula to add to the passed formula to sub-formulas of the received formulas, which are responsible for its occurrence
_mightBeConjunction	true, if the formula to add might be a conjunction.

Returns: A pair to the position where the formula to add has been inserted (or its first sub-formula which has not yet been in the passed formula, in case the formula to add is a conjunction), and a Boolean stating whether anything has been added to the passed formula.

Definition at line 341 of file Module.cpp.

Here is the call graph for this function:

◆ addSubformulaToPassedFormula() [3/4]

std::pair<ModuleInput::iterator,bool> smtrat::Module::addSubformulaToPassedFormula	(	const FormulaT &	_formula,
		const FormulaT &	_origin
	)

inlineprotectedinherited

Adds the given formula to the passed formula.

Parameters

_formula	The formula to add to the passed formula.
_origin	The sub-formula of the received formula being responsible for the occurrence of the formula to add to the passed formula.

Returns: A pair to the position where the formula to add has been inserted (or its first sub-formula which has not yet been in the passed formula, in case the formula to add is a conjunction), and a Boolean stating whether anything has been added to the passed formula.

Definition at line 901 of file Module.h.

Here is the call graph for this function:

◆ addSubformulaToPassedFormula() [4/4]

std::pair<ModuleInput::iterator,bool> smtrat::Module::addSubformulaToPassedFormula	(	const FormulaT &	_formula,
		const std::shared_ptr< std::vector< FormulaT >> &	_origins
	)

inlineprotectedinherited

Adds the given formula to the passed formula.

Parameters

_formula	The formula to add to the passed formula.
_origins	The link of the formula to add to the passed formula to sub-formulas of the received formulas, which are responsible for its occurrence

Returns: A pair to the position where the formula to add has been inserted (or its first sub-formula which has not yet been in the passed formula, in case the formula to add is a conjunction), and a Boolean stating whether anything has been added to the passed formula.

Definition at line 887 of file Module.h.

Here is the call graph for this function:

◆ addXorClauses()

template<class Settings >

void smtrat::SATModule< Settings >::addXorClauses	(	const Minisat::vec< Minisat::Lit > &	_literals,
		const Minisat::vec< Minisat::Lit > &	_negLiterals,
		int	_from,
		bool	_numOfNegatedLitsEven,
		unsigned	_type,
		Minisat::vec< Minisat::Lit > &	_clause,
		const FormulaT &	_original,
		typename FormulaCNFInfosMap::iterator	_formulaCNFInfoIter
	)

private

◆ allModels()

const std::vector<Model>& smtrat::Module::allModels ( ) const

inlineinherited

Returns: All satisfying assignments, if existent.

Definition at line 471 of file Module.h.

Here is the caller graph for this function:

◆ analyze()

template<class Settings >

bool smtrat::SATModule< Settings >::analyze	(	Minisat::CRef	confl,
		Minisat::vec< Minisat::Lit > &	out_learnt,
		int &	out_btlevel
	)

private

analyze : (confl : Clause*) (out_learnt : vec<Lit>&) (out_btlevel : int&) -> [void]

Description: Analyze conflict and produce a reason clause.

Pre-conditions:

'out_learnt' is assumed to be cleared.
Current decision level must be greater than root level.

Post-conditions:

'out_learnt[0]' is the asserting literal at level 'out_btlevel'.
If out_learnt.size() > 1 then 'out_learnt[1]' has the greatest decision level of the rest of literals. There may be others from the same level though.

Parameters

confl	A reference to the conflicting clause.
out_learnt	The asserting clause derived by this method.
out_btlevel	The level to backtrack to according the analysis of this method.

Returns: true, if the asserting clause does not equal the conflict clause given by confl

◆ anAnswerFound()

bool smtrat::Module::anAnswerFound ( ) const

inlineprotectedinherited

Checks for all antecedent modules and those which run in parallel with the same antecedent modules, whether one of them has determined a result.

Returns: True, if one of them has determined a result.

Definition at line 737 of file Module.h.

Here is the caller graph for this function:

◆ answerFound()

const smtrat::Conditionals& smtrat::Module::answerFound ( ) const

inlineinherited

Returns: A vector of Booleans: If any of them is true, we have to terminate a running check procedure.

Definition at line 597 of file Module.h.

Here is the caller graph for this function:

◆ attachClause()

template<class Settings >

void smtrat::SATModule< Settings >::attachClause ( Minisat::CRef cr )

private

Attach a clause to watcher lists.

Parameters

cr	[Minisat related code]

◆ backendsModel()

const Model & smtrat::Module::backendsModel ( ) const

protectedinherited

Stores the model of a backend which determined satisfiability of the passed formula in the model of this module.

Definition at line 630 of file Module.cpp.

Here is the call graph for this function:

◆ bool_satisfied()

template<class Settings >

bool smtrat::SATModule< Settings >::bool_satisfied ( const Minisat::Clause & c ) const

private

◆ bool_value() [1/2]

template<class Settings >

Minisat::lbool smtrat::SATModule< Settings >::bool_value ( Minisat::Lit p ) const

inlineprivate

Definition at line 1023 of file SATModule.h.

Here is the call graph for this function:

◆ bool_value() [2/2]

template<class Settings >

Minisat::lbool smtrat::SATModule< Settings >::bool_value ( Minisat::Var x ) const

inlineprivate

Definition at line 920 of file SATModule.h.

Here is the caller graph for this function:

◆ branchAt() [1/4]

bool smtrat::Module::branchAt	(	carl::Variable::Arg	_var,
		const Rational &	_value,
		bool	_leftCaseWeak = `true`,
		bool	_preferLeftCase = `true`,
		bool	_useReceivedFormulaAsPremise = `false`,
		const std::vector< FormulaT > &	_premise = `std::vector<FormulaT>()`
	)

inlineprotectedinherited

Definition at line 1098 of file Module.h.

Here is the call graph for this function:

◆ branchAt() [2/4]

bool smtrat::Module::branchAt	(	carl::Variable::Arg	_var,
		const Rational &	_value,
		std::vector< FormulaT > &&	_premise,
		bool	_leftCaseWeak = `true`,
		bool	_preferLeftCase = `true`,
		bool	_useReceivedFormulaAsPremise = `false`
	)

inlineprotectedinherited

Definition at line 1093 of file Module.h.

Here is the call graph for this function:

◆ branchAt() [3/4]

bool smtrat::Module::branchAt	(	const Poly &	_polynomial,
		bool	_integral,
		const Rational &	_value,
		bool	_leftCaseWeak = `true`,
		bool	_preferLeftCase = `true`,
		bool	_useReceivedFormulaAsPremise = `false`,
		const std::vector< FormulaT > &	_premise = `std::vector<FormulaT>()`
	)

inlineprotectedinherited

Definition at line 1088 of file Module.h.

Here is the call graph for this function:

◆ branchAt() [4/4]

bool smtrat::Module::branchAt	(	const Poly &	_polynomial,
		bool	_integral,
		const Rational &	_value,
		std::vector< FormulaT > &&	_premise,
		bool	_leftCaseWeak = `true`,
		bool	_preferLeftCase = `true`,
		bool	_useReceivedFormulaAsPremise = `false`
	)

protectedinherited

Adds a lemmas which provoke a branching for the given variable at the given value, if this module returns Unknown and there exists a preceding SATModule.

Note that the given value is rounded down and up, if the given variable is integer-valued.

Parameters

_polynomial	The variable to branch for.
_integral	A flag being true, if all variables in the polynomial to branch for are integral.
_value	The value to branch at.
_premise	The sub-formulas of the received formula from which the branch is followed. Note, that a premise is not necessary, as every branch is a valid formula. But a premise can prevent from branching unnecessarily.
_leftCaseWeak	true, if a branching in the form of (or (<= p b) (> p b)) is desired. false, if a branching in the form of (or (< p b) (>= p b)) is desired.
_preferLeftCase	true, if the left case (polynomial less(or equal) 0 shall be chosen first. false, otherwise.
_useReceivedFormulaAsPremise	true, if the whole received formula should be used as premise

Definition at line 478 of file Module.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ budgetOff()

template<class Settings >

void smtrat::SATModule< Settings >::budgetOff ( )

inlineprivate

[Minisat related code]

Definition at line 1102 of file SATModule.h.

◆ cancelAssignmentUntil()

template<class Settings >

void smtrat::SATModule< Settings >::cancelAssignmentUntil ( int level )

private

Revert the variables assignment until a given level (keeping all assignments at 'level')

Parameters

level The level to backtrack to

◆ cancelIncludingLiteral()

template<class Settings >

void smtrat::SATModule< Settings >::cancelIncludingLiteral ( Minisat::Lit lit )

private

◆ cancelUntil()

template<class Settings >

void smtrat::SATModule< Settings >::cancelUntil	(	int	level,
		bool	force = `false`
	)

private

Revert to the state at given level (keeping all assignments at 'level' but not beyond).

Parameters

level The level to backtrack to.

◆ check()

Answer smtrat::Module::check	(	bool	_final = `false`,
		bool	_full = `true`,
		carl::Variable	_objective = `carl::Variable::NO_VARIABLE`
	)

virtualinherited

Checks the received formula for consistency.

Note, that this is an implementation of the satisfiability check of the conjunction of the so far received formulas, which does actually nothing but passing the problem to its backends. This implementation is only used internally and must be overwritten by any derived module.

Parameters

_final	true, if this satisfiability check will be the last one (for a global sat-check), if its result is SAT
_full	false, if this module should avoid too expensive procedures and rather return unknown instead.
_objective	if not set to NO_VARIABLE, the module should find an assignment minimizing this objective variable; otherwise any assignment is good.

Returns: True, if the received formula is satisfiable; False, if the received formula is not satisfiable; Unknown, otherwise.

Reimplemented in smtrat::PModule.

Definition at line 86 of file Module.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ checkAbstractionsConsistency()

template<class Settings >

void smtrat::SATModule< Settings >::checkAbstractionsConsistency ( )

inlineprivate

Definition at line 1196 of file SATModule.h.

Here is the call graph for this function:

◆ checkCore()

template<class Settings >

Answer smtrat::SATModule< Settings >::checkCore ( )

virtual

Checks the received formula for consistency.

Returns: SAT, if the received formula is satisfiable; UNSAT, if the received formula is not satisfiable; Unknown, otherwise.

Reimplemented from smtrat::Module.

◆ checkFormula()

template<class Settings >

Minisat::lbool smtrat::SATModule< Settings >::checkFormula ( )

private

Checks the received formula for consistency.

Returns: l_True, if the received formula is satisfiable; l_False, if the received formula is not satisfiable; l_Undef, otherwise.

◆ checkGarbage() [1/2]

template<class Settings >

void smtrat::SATModule< Settings >::checkGarbage ( double gf )

inlineprivate

[Minisat related code]

Parameters

gf	[Minisat related code]

Definition at line 1134 of file SATModule.h.

Here is the call graph for this function:

◆ checkGarbage() [2/2]

template<class Settings >

void smtrat::SATModule< Settings >::checkGarbage ( void )

inlineprivate

[Minisat related code]

Definition at line 1143 of file SATModule.h.

◆ checkInfSubsetForMinimality()

void smtrat::Module::checkInfSubsetForMinimality	(	std::vector< FormulaSetT >::const_iterator	_infsubset,
		const std::string &	_filename = `"smaller_muses"`,
		unsigned	_maxSizeDifference = `1`
	)		const

inherited

Checks the given infeasible subset for minimality by storing all subsets of it, which have a smaller size which differs from the size of the infeasible subset not more than the given threshold.

Parameters

_infsubset	The infeasible subset to check for minimality.
_filename	The name of the file to store the infeasible subsets in order to be able to check their infeasibility.
_maxSizeDifference	The maximal difference between the sizes of the subsets compared to the size of the infeasible subset.

Definition at line 1018 of file Module.cpp.

Here is the call graph for this function:

◆ checkModel()

unsigned smtrat::Module::checkModel ( ) const

protectedinherited

Returns: false, if the current model of this module does not satisfy the current given formula; true, if it cannot be said whether the model satisfies the given formula.

Definition at line 588 of file Module.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ claBumpActivity()

template<class Settings >

void smtrat::SATModule< Settings >::claBumpActivity ( Minisat::Clause & c )

inlineprivate

Increase a clause with the current 'bump' value.

Parameters

c	[Minisat related code]

Definition at line 1492 of file SATModule.h.

Here is the call graph for this function:

◆ claDecayActivity()

template<class Settings >

void smtrat::SATModule< Settings >::claDecayActivity ( )

inlineprivate

Decay all clauses with the specified factor.

Implemented by increasing the 'bump' value instead.

Definition at line 1483 of file SATModule.h.

◆ cleanModel()

void smtrat::Module::cleanModel ( ) const

inlineprotectedinherited

Substitutes variable occurrences by its model value in the model values of other variables.

Definition at line 771 of file Module.h.

◆ cleanUpAfterOptimizing()

template<class Settings >

void smtrat::SATModule< Settings >::cleanUpAfterOptimizing ( const std::vector< Minisat::CRef > & _excludedAssignments )

◆ clearInterrupt()

template<class Settings >

void smtrat::SATModule< Settings >::clearInterrupt ( )

inlineprivate

Clear interrupt indicator flag.

Definition at line 1118 of file SATModule.h.

◆ clearLearnts()

template<class Settings >

void smtrat::SATModule< Settings >::clearLearnts ( int n )

private

◆ clearLemmas()

void smtrat::Module::clearLemmas ( )

inlineinherited

Deletes all yet found lemmas.

Definition at line 550 of file Module.h.

Here is the caller graph for this function:

◆ clearModel()

void smtrat::Module::clearModel ( ) const

inlineprotectedinherited

Clears the assignment, if any was found.

Definition at line 749 of file Module.h.

Here is the caller graph for this function:

◆ clearModels()

void smtrat::Module::clearModels ( ) const

inlineprotectedinherited

Clears all assignments, if any was found.

Definition at line 758 of file Module.h.

Here is the call graph for this function:

◆ clearPassedFormula()

void smtrat::Module::clearPassedFormula ( )

protectedinherited

Definition at line 850 of file Module.cpp.

Here is the call graph for this function:

◆ collectOrigins() [1/2]

void smtrat::Module::collectOrigins	(	const FormulaT &	_formula,
		FormulaSetT &	_origins
	)		const

inherited

Definition at line 980 of file Module.cpp.

Here is the call graph for this function:

◆ collectOrigins() [2/2]

void smtrat::Module::collectOrigins	(	const FormulaT &	_formula,
		FormulasT &	_origins
	)		const

inherited

Collects the formulas in the given formula, which are part of the received formula.

If the given formula directly occurs in the received formula, it is inserted into the given set. Otherwise, the given formula must be of type AND and all its sub-formulas part of the received formula. Hence, they will be added to the given set.

Parameters

_formula	The formula from which to collect the formulas being sub-formulas of the received formula (origins).
_origins	The set in which to store the origins.

Definition at line 960 of file Module.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ collectStats()

template<class Settings >

void smtrat::SATModule< Settings >::collectStats ( )

Collects the taken statistics.

◆ collectTheoryPropagations()

void smtrat::Module::collectTheoryPropagations ( )

inherited

Definition at line 928 of file Module.cpp.

◆ computeAdvancedLemmas()

template<class Settings >

void smtrat::SATModule< Settings >::computeAdvancedLemmas ( )

private

◆ constraintsToInform()

const carl::FastSet<FormulaT>& smtrat::Module::constraintsToInform ( ) const

inlineinherited

Returns: The constraints which the backends must be informed about.

Definition at line 496 of file Module.h.

◆ constructLemmas()

template<class Settings >

void smtrat::SATModule< Settings >::constructLemmas ( )

private

◆ createLiteral()

template<class Settings >

Minisat::Lit smtrat::SATModule< Settings >::createLiteral	(	const FormulaT &	_formula,
		const FormulaT &	_origin = `FormulaT(carl::FormulaType::TRUE)`,
		bool	_decisionRelevant = `true`
	)

private

Creates or simply returns the literal belonging to the formula being the first argument.

Parameters

_formula	The formula to get the literal for.
_origin	The origin of the formula to get the literal for.
_decisionRelevant	true, if the variable of the literal needs to be involved in the decision process of the SAT solving.

Returns: The corresponding literal.

Here is the caller graph for this function:

◆ currentlySatisfied()

virtual unsigned smtrat::Module::currentlySatisfied ( const FormulaT & ) const

inlinevirtualinherited

Returns: 0, if the given formula is conflicted by the current model; 1, if the given formula is satisfied by the current model; 2, otherwise; 3, if we do not know anything (default)

Reimplemented in smtrat::LRAModule< Settings >, smtrat::LRAModule< smtrat::LRASettings1 >, and smtrat::LRAModule< smtrat::LRASettingsICP >.

Definition at line 372 of file Module.h.

◆ currentlySatisfiedByBackend()

unsigned smtrat::Module::currentlySatisfiedByBackend ( const FormulaT & _formula ) const

inherited

Returns: 0, if the given formula is conflicted by the current model; 1, if the given formula is satisfied by the current model; 2, otherwise 3, if we do not know anything (default)

Definition at line 296 of file Module.cpp.

◆ decisionLevel()

template<class Settings >

int smtrat::SATModule< Settings >::decisionLevel ( ) const

inlineprivate

Returns: The current decision level.

Definition at line 1582 of file SATModule.h.

Here is the call graph for this function:

◆ decrementLearntSizeAdjustCnt()

template<class Settings >

void smtrat::SATModule< Settings >::decrementLearntSizeAdjustCnt ( )

private

[Minisat related code]

◆ decrementTseitinShadowOccurrences()

template<class Settings >

void smtrat::SATModule< Settings >::decrementTseitinShadowOccurrences ( signed _var )

inlineprivate

Definition at line 1218 of file SATModule.h.

Here is the call graph for this function:

◆ deinform()

void smtrat::Module::deinform ( const FormulaT & _constraint )

inherited

The inverse of informing about a constraint.

All data structures which were kept regarding this constraint are going to be removed. Note, that this makes only sense if it is not likely enough that a formula with this constraint must be solved again.

Parameters

_constraint The constraint to remove from internal data structures.

Definition at line 124 of file Module.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ deinformCore()

virtual void smtrat::Module::deinformCore ( [[maybe_unused] ] const FormulaT & _constraint )

inlineprotectedvirtualinherited

The inverse of informing about a constraint.

All data structures which were kept regarding this constraint are going to be removed. Note, that this makes only sense if it is not likely enough that a formula with this constraint must be solved again.

Parameters

_constraint The constraint to remove from internal data structures.

Definition at line 695 of file Module.h.

Here is the caller graph for this function:

◆ detachClause()

template<class Settings >

void smtrat::SATModule< Settings >::detachClause	(	Minisat::CRef	cr,
		bool	strict = `false`
	)

private

Detach a clause to watcher lists.

Parameters

cr	[Minisat related code]
strict	[Minisat related code]

◆ determine_smallest_origin()

size_t smtrat::Module::determine_smallest_origin ( const std::vector< FormulaT > & origins ) const

protectedinherited

Parameters

origins A vector of sets of origins.

Returns: The index of the smallest (regarding the size of the sets) element of origins

Definition at line 403 of file Module.cpp.

◆ drand()

template<class Settings >

static double smtrat::SATModule< Settings >::drand ( double & seed )

inlinestaticprivate

Parameters

seed	[Minisat related code]

Returns: A random float 0 <= x < 1. Seed must never be 0.

Definition at line 1667 of file SATModule.h.

Here is the caller graph for this function:

◆ enqueue()

template<class Settings >

bool smtrat::SATModule< Settings >::enqueue	(	Minisat::Lit	p,
		Minisat::CRef	from = `Minisat::CRef_Undef`
	)

inlineprivate

Test if fact 'p' contradicts current state, enqueue otherwise.

NOTE: enqueue does not set the ok flag! (only public methods do)

Parameters

p	[Minisat related code]
from	[Minisat related code]

Returns: [Minisat related code]

Definition at line 1254 of file SATModule.h.

Here is the call graph for this function:

◆ eraseSubformulaFromPassedFormula()

ModuleInput::iterator smtrat::Module::eraseSubformulaFromPassedFormula	(	ModuleInput::iterator	_subformula,
		bool	_ignoreOrigins = `false`
	)

protectedvirtualinherited

Removes everything related to the sub-formula to remove from the passed formula in the backends of this module.

Afterwards the sub-formula is removed from the passed formula.

Parameters

_subformula	The sub-formula to remove from the passed formula.
_ignoreOrigins	True, if the sub-formula shall be removed regardless of its origins (should only be applied with expertise).

Returns

Reimplemented in smtrat::ICPModule< Settings >, smtrat::ICPModule< smtrat::ICPSettings1 >, and smtrat::ICPModule< smtrat::ICPSettings4 >.

Definition at line 807 of file Module.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ excludeNotReceivedVariablesFromModel()

void smtrat::Module::excludeNotReceivedVariablesFromModel ( ) const

inherited

Excludes all variables from the current model, which do not occur in the received formula.

Definition at line 884 of file Module.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ expPositionsCorrect()

template<class Settings >

bool smtrat::SATModule< Settings >::expPositionsCorrect ( ) const

private

◆ findBestOrigin()

std::vector< FormulaT >::const_iterator smtrat::Module::findBestOrigin ( const std::vector< FormulaT > & _origins ) const

protectedinherited

Parameters

_origins

Returns

Definition at line 691 of file Module.cpp.

Here is the caller graph for this function:

◆ firstSubformulaToPass()

ModuleInput::const_iterator smtrat::Module::firstSubformulaToPass ( ) const

inlineinherited

Returns: The position of the first sub-formula in the passed formula, which has not yet been considered for a consistency check of the backends.

Definition at line 581 of file Module.h.

Here is the caller graph for this function:

◆ firstUncheckedReceivedSubformula()

ModuleInput::const_iterator smtrat::Module::firstUncheckedReceivedSubformula ( ) const

inlineinherited

Returns: The position of the first (by this module) unchecked sub-formula of the received formula.

Definition at line 573 of file Module.h.

◆ foundAnswer()

Answer smtrat::Module::foundAnswer ( Answer _answer )

privateinherited

Sets the solver state to the given answer value.

This method also fires the flag given by the antecessor module of this module to true, if the given answer value is not Unknown.

Parameters

_answer The found answer.

Definition at line 856 of file Module.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ freeSplittingVariable()

static void smtrat::Module::freeSplittingVariable ( const FormulaT & _splittingVariable )

inlinestaticinherited

Definition at line 509 of file Module.h.

◆ fullAssignment()

template<class Settings >

bool smtrat::SATModule< Settings >::fullAssignment ( )

private

Returns: true, if the current assignment is a full one.

◆ garbageCollect()

template<class Settings >

void smtrat::SATModule< Settings >::garbageCollect ( )

private

[Minisat related code]

Here is the caller graph for this function:

◆ generateTrivialInfeasibleSubset()

void smtrat::Module::generateTrivialInfeasibleSubset ( )

inlineprotectedinherited

Stores the trivial infeasible subset being the set of received formulas.

Definition at line 909 of file Module.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ getBackendsAllModels()

void smtrat::Module::getBackendsAllModels ( ) const

protectedinherited

Stores all models of a backend in the list of all models of this module.

Definition at line 669 of file Module.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ getBackendsModel()

void smtrat::Module::getBackendsModel ( ) const

protectedinherited

Definition at line 652 of file Module.cpp.

Here is the caller graph for this function:

◆ getClause()

template<class Settings >

Minisat::Clause& smtrat::SATModule< Settings >::getClause ( Minisat::CRef cr )

inlineprivate

Definition at line 1526 of file SATModule.h.

◆ getInfeasibleSubsets() [1/2]

void smtrat::Module::getInfeasibleSubsets ( )

protectedinherited

Copies the infeasible subsets of the passed formula.

Definition at line 596 of file Module.cpp.

Here is the caller graph for this function:

◆ getInfeasibleSubsets() [2/2]

std::vector< FormulaSetT > smtrat::Module::getInfeasibleSubsets ( const Module & _backend ) const

protectedinherited

Get the infeasible subsets the given backend provides.

Note, that an infeasible subset in a backend contains sub formulas of the passed formula and an infeasible subset of this module contains sub formulas of the received formula. In this method the LATTER is returned.

Parameters

_backend The backend from which to obtain the infeasible subsets.

Returns: The infeasible subsets the given backend provides.

Definition at line 709 of file Module.cpp.

Here is the call graph for this function:

◆ getInformationRelevantFormulas()

const std::set< FormulaT > & smtrat::Module::getInformationRelevantFormulas ( )

protectedinherited

Gets all InformationRelevantFormulas.

Returns: Set of all formulas

Definition at line 1074 of file Module.cpp.

Here is the call graph for this function:

◆ getLiteral()

template<class Settings >

Minisat::Lit smtrat::SATModule< Settings >::getLiteral ( const FormulaT & _formula ) const

private

◆ getModelEqualities()

std::list< std::vector< carl::Variable > > smtrat::Module::getModelEqualities ( ) const

virtualinherited

Partition the variables from the current model into equivalence classes according to their assigned value.

The result is a set of equivalence classes of variables where all variables within one class are assigned the same value. Note that the number of classes may not be minimal, i.e. two classes may actually be equivalent.

Returns: Equivalence classes.

Definition at line 308 of file Module.cpp.

Here is the caller graph for this function:

◆ getOrigins() [1/3]

void smtrat::Module::getOrigins	(	const FormulaT &	_formula,
		FormulaSetT &	_origins
	)		const

inlineprotectedinherited

Parameters

_formula
_origins

Definition at line 968 of file Module.h.

Here is the call graph for this function:

◆ getOrigins() [2/3]

void smtrat::Module::getOrigins	(	const FormulaT &	_formula,
		FormulasT &	_origins
	)		const

inlineprotectedinherited

Parameters

_formula
_origins

Definition at line 955 of file Module.h.

Here is the call graph for this function:

◆ getOrigins() [3/3]

const FormulaT& smtrat::Module::getOrigins ( ModuleInput::const_iterator _formula ) const

inlineprotectedinherited

Gets the origins of the passed formula at the given position.

Parameters

_formula The position of a formula in the passed formulas.

Returns: The origins of the passed formula at the given position.

Definition at line 808 of file Module.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ getReceivedFormulaSimplified()

std::pair< bool, FormulaT > smtrat::Module::getReceivedFormulaSimplified ( )

virtualinherited

Returns: A pair of a Boolean and a formula, where the Boolean is true, if the received formula could be simplified to an equisatisfiable formula. The formula is equisatisfiable to this module's reveived formula, if the Boolean is true.

Reimplemented in smtrat::PModule.

Definition at line 945 of file Module.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ handleConflict()

template<class Settings >

void smtrat::SATModule< Settings >::handleConflict ( Minisat::CRef _confl )

private

Handles conflict.

Parameters

conf	conflict clause

Returns: if return is not l_True, search can be aborted

Here is the caller graph for this function:

◆ handleTheoryConflict()

template<class Settings >

void smtrat::SATModule< Settings >::handleTheoryConflict ( const mcsat::Explanation & explanation )

inlineprivate

Definition at line 987 of file SATModule.h.

Here is the call graph for this function:

◆ hasLemmas()

bool smtrat::Module::hasLemmas ( )

inlineinherited

Checks whether this module or any of its backends provides any lemmas.

Definition at line 532 of file Module.h.

◆ hasValidInfeasibleSubset()

bool smtrat::Module::hasValidInfeasibleSubset ( ) const

inherited

Returns: true, if the module has at least one valid infeasible subset, that is all its elements are sub-formulas of the received formula (pointer must be equal).

Definition at line 1000 of file Module.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ id()

std::size_t smtrat::Module::id ( ) const

inlineinherited

Returns: A unique ID to identify this module instance.

Definition at line 396 of file Module.h.

◆ incrementTseitinShadowOccurrences()

template<class Settings >

void smtrat::SATModule< Settings >::incrementTseitinShadowOccurrences ( signed _var )

inlineprivate

Definition at line 1229 of file SATModule.h.

Here is the call graph for this function:

◆ infeasibleSubsets()

const std::vector<FormulaSetT>& smtrat::Module::infeasibleSubsets ( ) const

inlineinherited

Returns: The infeasible subsets of the set of received formulas (empty, if this module has not detected unsatisfiability of the conjunction of received formulas.

Definition at line 480 of file Module.h.

Here is the caller graph for this function:

◆ inform()

bool smtrat::Module::inform ( const FormulaT & _constraint )

inherited

Informs the module about the given constraint.

It should be tried to inform this module about any constraint it could receive eventually before assertSubformula is called (preferably for the first time, but at least before adding a formula containing that constraint).

Parameters

_constraint The constraint to inform about.

Returns: false, if it can be easily decided whether the given constraint is inconsistent; true, otherwise.

Definition at line 117 of file Module.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ informBackends()

void smtrat::Module::informBackends ( const FormulaT & _constraint )

inlineprotectedinherited

Informs all backends of this module about the given constraint.

Parameters

_constraint The constraint to inform about.

Definition at line 836 of file Module.h.

◆ informCore()

virtual bool smtrat::Module::informCore ( [[maybe_unused] ] const FormulaT & _constraint )

inlineprotectedvirtualinherited

Informs the module about the given constraint.

It should be tried to inform this module about any constraint it could receive eventually before assertSubformula is called (preferably for the first time, but at least before adding a formula containing that constraint).

Parameters

_constraint The constraint to inform about.

Returns: false, if it can be easily decided whether the given constraint is inconsistent; true, otherwise.

Definition at line 684 of file Module.h.

Here is the caller graph for this function:

◆ informedConstraints()

const carl::FastSet<FormulaT>& smtrat::Module::informedConstraints ( ) const

inlineinherited

Returns: The position of the first constraint of which no backend has been informed about.

Definition at line 504 of file Module.h.

Here is the caller graph for this function:

◆ init()

void smtrat::Module::init ( )

virtualinherited

Informs all backends about the so far encountered constraints, which have not yet been communicated.

This method must not be called twice and only before the first runBackends call.

Reimplemented in smtrat::PBPPModule< Settings >, smtrat::PBGaussModule< Settings >, smtrat::NRAILModule< Settings >, smtrat::NewCoveringModule< Settings >, smtrat::NewCADModule< Settings >, smtrat::LRAModule< Settings >, smtrat::LRAModule< smtrat::LRASettings1 >, smtrat::LRAModule< smtrat::LRASettingsICP >, smtrat::IntBlastModule< Settings >, smtrat::FPPModule< Settings >, smtrat::CurryModule< Settings >, and smtrat::BVModule< Settings >.

Definition at line 234 of file Module.cpp.

Here is the call graph for this function:

◆ insertVarOrder()

template<class Settings >

void smtrat::SATModule< Settings >::insertVarOrder ( Minisat::Var x )

inlineprivate

Insert a variable in the decision order priority queue.

Parameters

x	[Minisat related code]

Definition at line 1161 of file SATModule.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ interrupt()

template<class Settings >

void smtrat::SATModule< Settings >::interrupt ( )

inlineprivate

Trigger a (potentially asynchronous) interruption of the solver.

Definition at line 1110 of file SATModule.h.

◆ irand()

template<class Settings >

static int smtrat::SATModule< Settings >::irand	(	double &	seed,
		int	size
	)

inlinestaticprivate

Parameters

seed	[Minisat related code]
size	[Minisat related code]

Returns: A random integer 0 <= x < size. Seed must never be 0.

Definition at line 1680 of file SATModule.h.

Here is the call graph for this function:

◆ is_minimizing()

bool smtrat::Module::is_minimizing ( ) const

inlineinherited

Definition at line 623 of file Module.h.

◆ isLemmaLevel()

bool smtrat::Module::isLemmaLevel ( LemmaLevel level )

protectedinherited

Checks if current lemma level is greater or equal to given level.

Parameters

level Level to check.

Definition at line 1079 of file Module.cpp.

Here is the call graph for this function:

◆ isPreprocessor()

bool smtrat::Module::isPreprocessor ( ) const

inlineinherited

Returns: true, if this module is a preprocessor that is a module, which simplifies its received formula to an equisatisfiable formula being passed to its backends. The simplified formula can be obtained with getReceivedFormulaSimplified().

Definition at line 607 of file Module.h.

◆ learnTheoryConflicts()

template<class Settings >

void smtrat::SATModule< Settings >::learnTheoryConflicts ( )

private

Adds the clauses representing all conflicts generated by all backends.

Returns: A reference to the clause representing the best infeasible subset.

◆ lemmas()

const std::vector<Lemma>& smtrat::Module::lemmas ( ) const

inlineinherited

Returns: A constant reference to the lemmas being valid formulas this module or its backends made.

Definition at line 565 of file Module.h.

Here is the caller graph for this function:

◆ level() [1/2]

template<class Settings >

int smtrat::SATModule< Settings >::level ( const Minisat::vec< Minisat::Lit > & ) const

private

Parameters

_clause The clause to get the highest decision level in which assigned one of its literals has been assigned.

Returns: The highest decision level which assigned a literal of the given clause.

◆ level() [2/2]

template<class Settings >

int smtrat::SATModule< Settings >::level ( Minisat::Var x ) const

inlineprivate

Parameters

x	The variable for which we to get the level in which it has been assigned to a value.

Returns: The level in which the variable has been assigned, if it is not unassigned.

Definition at line 1611 of file SATModule.h.

Here is the caller graph for this function:

◆ litRedundant()

template<class Settings >

bool smtrat::SATModule< Settings >::litRedundant	(	Minisat::Lit	p,
		uint32_t	abstract_levels
	)

private

Check if 'p' can be removed.

'abstract_levels' is used to abort early if the algorithm is visiting literals at levels that cannot be removed later.

Parameters

p	[Minisat related code]
abstract_levels	[Minisat related code]

Returns: [Minisat related code]

◆ locked()

template<class Settings >

bool smtrat::SATModule< Settings >::locked ( const Minisat::Clause & c )

inlineprivate

Parameters

c	[Minisat related code]

Returns: TRUE if a clause is a reason for some implication in the current state.

Definition at line 1534 of file SATModule.h.

Here is the call graph for this function:

◆ luby()

template<class Settings >

static double smtrat::SATModule< Settings >::luby	(	double	y,
		int	x
	)

staticprivate

Finite subsequences of the Luby-sequence:

0: 1 1: 1 1 2 2: 1 1 2 1 1 2 4 3: 1 1 2 1 1 2 4 1 1 2 1 1 2 4 8 ...

Parameters

y
x

Returns

◆ mapVar()

template<class Settings >

static Minisat::Var smtrat::SATModule< Settings >::mapVar	(	Minisat::Var	x,
		Minisat::vec< Minisat::Var > &	map,
		Minisat::Var &	max
	)

staticprivate

[Minisat related code]

Parameters

x	[Minisat related code]
map	[Minisat related code]
max	[Minisat related code]

Returns: [Minisat related code]

◆ maxActivity()

template<class Settings >

double smtrat::SATModule< Settings >::maxActivity ( ) const

inlineprivate

Returns: The maximum of all activities of the occurring literals.

Definition at line 1412 of file SATModule.h.

Here is the call graph for this function:

◆ merge()

std::vector< FormulaT > smtrat::Module::merge	(	const std::vector< FormulaT > &	_vecSetA,
		const std::vector< FormulaT > &	_vecSetB
	)		const

protectedinherited

Merges the two vectors of sets into the first one.

({a,b},{a,c}) and ({b,d},{b}) -> ({a,b,d},{a,b},{a,b,c,d},{a,b,c})

Parameters

_vecSetA	A vector of sets of constraints.
_vecSetB	A vector of sets of constraints.

Returns: The vector being the two given vectors merged.

Definition at line 377 of file Module.cpp.

◆ min_theory_level()

template<class Settings >

int smtrat::SATModule< Settings >::min_theory_level ( Minisat::Var x ) const

inlineprivate

Definition at line 1620 of file SATModule.h.

Here is the call graph for this function:

◆ model()

const Model& smtrat::Module::model ( ) const

inlineinherited

Returns: The assignment of the current satisfiable result, if existent.

Definition at line 463 of file Module.h.

Here is the caller graph for this function:

◆ modelsDisjoint()

bool smtrat::Module::modelsDisjoint	(	const Model &	_modelA,
		const Model &	_modelB
	)

staticprotectedinherited

Checks whether there is no variable assigned by both models.

Parameters

_modelA	The first model to check for.
_modelB	The second model to check for.

Returns: true, if there is no variable assigned by both models; false, otherwise.

Definition at line 611 of file Module.cpp.

◆ moduleName()

virtual std::string smtrat::Module::moduleName ( ) const

inlinevirtualinherited

Returns: The name of the given module type as name.

Definition at line 615 of file Module.h.

Here is the caller graph for this function:

◆ nAssigns()

template<class Settings >

int smtrat::SATModule< Settings >::nAssigns ( ) const

inlineprivate

Returns: The current number of assigned literals.

Definition at line 1042 of file SATModule.h.

Here is the call graph for this function:

◆ nClauses()

template<class Settings >

int smtrat::SATModule< Settings >::nClauses ( ) const

inlineprivate

Returns: The current number of original clauses.

Definition at line 1050 of file SATModule.h.

Here is the call graph for this function:

◆ newDecisionLevel()

template<class Settings >

void smtrat::SATModule< Settings >::newDecisionLevel ( )

inlineprivate

Begins a new decision level.

Definition at line 1213 of file SATModule.h.

Here is the call graph for this function:

◆ newVar()

template<class Settings >

Minisat::Var smtrat::SATModule< Settings >::newVar	(	bool	polarity = `true`,
		bool	dvar = `true`,
		double	_activity = `0`,
		bool	insertIntoHeap = `true`
	)

private

Creates a new SAT variable in the solver.

If 'decision' is cleared, variable will not be used as a decision variable (NOTE! This has effects on the meaning of a SATISFIABLE result).

Parameters

polarity	A flag, which is true, if the variable preferably is assigned to false.
dvar	A flag, which is true, if the variable to create needs to considered in the solving.
_activity	The initial activity of the variable to create.
_tseitinShadowed	A flag, which is true, if the variable to create is a sub-formula of a formula represented by a Tseitin variable.

Returns: The created Minisat variable.

◆ nFreeVars()

template<class Settings >

int smtrat::SATModule< Settings >::nFreeVars ( ) const

inlineprivate

Returns: [Minisat related code]

Definition at line 1074 of file SATModule.h.

Here is the call graph for this function:

◆ nLearnts()

template<class Settings >

int smtrat::SATModule< Settings >::nLearnts ( ) const

inlineprivate

Returns: The current number of learned clauses.

Definition at line 1058 of file SATModule.h.

Here is the call graph for this function:

◆ nVars()

template<class Settings >

int smtrat::SATModule< Settings >::nVars ( ) const

inlineprivate

Returns: The current number of variables.

Definition at line 1066 of file SATModule.h.

Here is the caller graph for this function:

◆ objective()

carl::Variable smtrat::Module::objective ( ) const

inlineinherited

Definition at line 619 of file Module.h.

◆ okay()

template<class Settings >

bool smtrat::SATModule< Settings >::okay ( ) const

inlineprivate

Returns: FALSE means solver is in a conflicting state

Definition at line 887 of file SATModule.h.

◆ originInReceivedFormula()

bool smtrat::Module::originInReceivedFormula ( const FormulaT & _origin ) const

protectedinherited

Definition at line 352 of file Module.cpp.

Here is the call graph for this function:

◆ passedFormulaBegin()

ModuleInput::iterator smtrat::Module::passedFormulaBegin ( )

inlineprotectedinherited

Returns: An iterator to the end of the passed formula. TODO: disable this method

Definition at line 780 of file Module.h.

Here is the call graph for this function:

◆ passedFormulaCorrect()

template<class Settings >

bool smtrat::SATModule< Settings >::passedFormulaCorrect ( ) const

private

Returns: true, if the passed formula coincides with the constraints whose abstractions (literals) are assigned to true.

◆ passedFormulaEnd()

ModuleInput::iterator smtrat::Module::passedFormulaEnd ( )

inlineprotectedinherited

Returns: An iterator to the end of the passed formula.

Definition at line 788 of file Module.h.

Here is the call graph for this function:

◆ pickBranchLit()

template<class Settings >

Minisat::Lit smtrat::SATModule< Settings >::pickBranchLit ( )

private

Returns: The next decision variable.

◆ pPassedFormula()

const ModuleInput* smtrat::Module::pPassedFormula ( ) const

inlineinherited

Returns: A pointer to the formula passed to the backends of this module.

Definition at line 447 of file Module.h.

Here is the caller graph for this function:

◆ pReceivedFormula()

const ModuleInput* smtrat::Module::pReceivedFormula ( ) const

inlineinherited

Returns: A pointer to the formula passed to this module.

Definition at line 431 of file Module.h.

◆ print() [1/2]

void smtrat::Module::print ( const std::string & _initiation = "***" ) const

inherited

Prints everything relevant of the solver.

Parameters

_initiation The line initiation.

Definition at line 1085 of file Module.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ print() [2/2]

template<class Settings >

void smtrat::SATModule< Settings >::print	(	std::ostream &	_out = `std::cout`,
		const std::string &	_init = `""`
	)		const

Prints everything.

Parameters

_out	The output stream where the answer should be printed.
_init	The line initiation.

Here is the caller graph for this function:

◆ printAllModels()

void smtrat::Module::printAllModels ( std::ostream & _out = std::cout )

inherited

Prints all assignments of this module satisfying its received formula if it satisfiable and this module could find an assignment.

Parameters

_out	The stream to print the assignment on.

Definition at line 1161 of file Module.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ printBooleanConstraintMap()

template<class Settings >

void smtrat::SATModule< Settings >::printBooleanConstraintMap	(	std::ostream &	_out = `std::cout`,
		const std::string &	_init = `""`
	)		const

Prints the literal to constraint map.

Parameters

_out	The output stream where the answer should be printed.
_init	The line initiation.

◆ printBooleanVarMap()

template<class Settings >

void smtrat::SATModule< Settings >::printBooleanVarMap	(	std::ostream &	_out = `std::cout`,
		const std::string &	_init = `""`
	)		const

Prints map of the Boolean within the SAT solver to the given Booleans.

Parameters

_out	The output stream where the answer should be printed.
_init	The line initiation.

◆ printClause() [1/2]

template<class Settings >

void smtrat::SATModule< Settings >::printClause	(	const Minisat::vec< Minisat::Lit > &	,
		bool	_withAssignment = `false`,
		std::ostream &	_out = `std::cout`,
		const std::string &	_init = `""`
	)		const

Prints the clause resulting from the given vector of literals.

Parameters

_clause	The reference of the clause.
_withAssignment	A flag indicating if true, that the assignments should be printed too.
_out	The output stream where the answer should be printed.
_init	The prefix of each printed line.

◆ printClause() [2/2]

template<class Settings >

void smtrat::SATModule< Settings >::printClause	(	Minisat::CRef	_clause,
		bool	_withAssignment = `false`,
		std::ostream &	_out = `std::cout`,
		const std::string &	_init = `""`
	)		const

Prints the clause at the given reference.

Parameters

_clause	The reference of the clause.
_withAssignment	A flag indicating if true, that the assignments should be printed too.
_out	The output stream where the answer should be printed.
_init	The prefix of each printed line.

◆ printClauseInformation()

template<class Settings >

void smtrat::SATModule< Settings >::printClauseInformation	(	std::ostream &	_out = `std::cout`,
		const std::string &	_init = `""`
	)		const

Prints the clause information.

Parameters

_out	The output stream where the answer should be printed.
_init	The line initiation.

◆ printClauses()

template<class Settings >

void smtrat::SATModule< Settings >::printClauses	(	const Minisat::vec< Minisat::CRef > &	_clauses,
		const std::string	_name,
		std::ostream &	_out = `std::cout`,
		const std::string &	_init = `""`,
		int	= `0`,
		bool	_withAssignment = `false`,
		bool	_onlyNotSatisfied = `false`
	)		const

Prints all given clauses.

Parameters

_clauses	The clauses to print.
_name	The name of the clauses to print. (e.g. learnts, clauses, ..)
_out	The output stream where the answer should be printed.
_init	The prefix of each printed line.
_from	The position of the first clause to print within the given vector of clauses.
_withAssignment	A flag indicating if true, that the assignments should be printed too.

◆ printConstraintLiteralMap()

template<class Settings >

void smtrat::SATModule< Settings >::printConstraintLiteralMap	(	std::ostream &	_out = `std::cout`,
		const std::string &	_init = `""`
	)		const

Prints the constraints to literal map.

Parameters

_out	The output stream where the answer should be printed.
_init	The line initiation.

◆ printCurrentAssignment()

template<class Settings >

void smtrat::SATModule< Settings >::printCurrentAssignment	(	std::ostream &	= `std::cout`,
		const std::string &	= `""`
	)		const

Prints the current assignment of the SAT solver.

Parameters

_out	The output stream where the answer should be printed.
_init	The line initiation.

◆ printDecisions()

template<class Settings >

void smtrat::SATModule< Settings >::printDecisions	(	std::ostream &	_out = `std::cout`,
		const std::string &	_init = `""`
	)		const

Prints the decisions the SAT solver has made.

Parameters

_out	The output stream where the answer should be printed.
_init	The line initiation.

◆ printFormulaCNFInfosMap()

template<class Settings >

void smtrat::SATModule< Settings >::printFormulaCNFInfosMap	(	std::ostream &	_out = `std::cout`,
		const std::string &	_init = `""`
	)		const

Prints the formulas to clauses map.

Parameters

_out	The output stream where the answer should be printed.
_init	The line initiation.

◆ printInfeasibleSubsets()

void smtrat::Module::printInfeasibleSubsets ( const std::string & _initiation = "***" ) const

inherited

Prints the infeasible subsets.

Parameters

_initiation The line initiation.

Definition at line 1136 of file Module.cpp.

Here is the caller graph for this function:

◆ printLiteralsActiveOccurrences()

template<class Settings >

void smtrat::SATModule< Settings >::printLiteralsActiveOccurrences	(	std::ostream &	_out = `std::cout`,
		const std::string &	_init = `""`
	)		const

Prints the literals' active occurrences in all clauses.

Parameters

_out	The output stream where the answer should be printed.
_init	The line initiation.

◆ printModel()

void smtrat::Module::printModel ( std::ostream & _out = std::cout ) const

inherited

Prints the assignment of this module satisfying its received formula if it satisfiable and this module could find an assignment.

Parameters

_out	The stream to print the assignment on.

Definition at line 1151 of file Module.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ printPassedFormula()

void smtrat::Module::printPassedFormula ( const std::string & _initiation = "***" ) const

inherited

Prints the vector of passed formula.

Parameters

_initiation The line initiation.

Definition at line 1118 of file Module.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ printPropagatedLemmas()

template<class Settings >

void smtrat::SATModule< Settings >::printPropagatedLemmas	(	std::ostream &	_out = `std::cout`,
		const std::string &	_init = `""`
	)		const

Prints the propagated lemmas for each variables which influence its value.

Parameters

_out	The output stream where the answer should be printed.
_init	The line initiation.

◆ printReceivedFormula()

void smtrat::Module::printReceivedFormula ( const std::string & _initiation = "***" ) const

inherited

Prints the vector of the received formula.

Parameters

_initiation The line initiation.

Definition at line 1105 of file Module.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ printSatState()

template<class Settings >

void smtrat::SATModule< Settings >::printSatState	(	std::ostream &	= `std::cout`,
		const std::string	= `""`
	)

private

[Minisat related code]

Parameters

std::cout	[Minisat related code]
[Minisat	related code]

◆ probablyLooping()

bool smtrat::Module::probablyLooping	(	const typename Poly::PolyType &	_branchingPolynomial,
		const Rational &	_branchingValue
	)		const

protectedinherited

Checks whether given the current branching value and branching variable/polynomial it is (highly) probable that this branching is part of an infinite loop of branchings.

Parameters

_branchingPolynomial	The polynomial to branch at (in most branching strategies this is just a variable).
_branchingValue	The value to branch at.

Returns: true, if this branching is probably part of an infinite loop of branchings; false, otherwise.

Definition at line 426 of file Module.cpp.

◆ processLemmas()

template<class Settings >

bool smtrat::SATModule< Settings >::processLemmas ( )

private

Adds clauses representing the lemmas which should be added to this SATModule.

This may provoke backtracking.

Returns: true, if any clause has been added.

◆ progressEstimate()

template<class Settings >

double smtrat::SATModule< Settings >::progressEstimate ( ) const

private

Returns: An estimation of the progress the SAT solver has been made, depending on how many assignments have been excluded and how many assignments are in general possible. The calculated value is between 0 and 1.

◆ propagate()

template<class Settings >

Minisat::CRef smtrat::SATModule< Settings >::propagate ( )

private

propagate : [void] -> [Clause*]

Description: Propagates all enqueued facts. If a conflict arises, the conflicting clause is returned, otherwise CRef_Undef.

Post-conditions:

the propagation queue is empty, even if there was a conflict.

Returns: A reference to the conflicting clause, if a conflict has been detected.

◆ propagateConsistently()

template<class Settings >

Minisat::CRef smtrat::SATModule< Settings >::propagateConsistently ( bool _checkWithTheory = true )

private

Propagate and check the consistency of the constraints, whose abstraction literals have been assigned to true.

Parameters

_madeTheoryCall A flag which is set to true, if at least one theory call has been made within this method.

Returns: A reference to a conflicting clause, if a clause has been added.

◆ propagateTheory()

template<class Settings >

void smtrat::SATModule< Settings >::propagateTheory ( )

private

◆ reason()

template<class Settings >

Minisat::CRef smtrat::SATModule< Settings >::reason ( Minisat::Var x )

private

Parameters

x	The variable to get the reason for it's assignment.

Returns: A reference to the clause, which implied the current assignment of this variable. It is not defined, if the assignment of the variable follows from a clause of size 0 or if the variable is unassigned.

Here is the caller graph for this function:

◆ rebuildOrderHeap()

template<class Settings >

void smtrat::SATModule< Settings >::rebuildOrderHeap ( )

private

[Minisat related code]

◆ receivedFormulaChecked()

void smtrat::Module::receivedFormulaChecked ( )

inlineinherited

Notifies that the received formulas has been checked.

Definition at line 589 of file Module.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ receivedFormulasAsInfeasibleSubset()

void smtrat::Module::receivedFormulasAsInfeasibleSubset ( ModuleInput::const_iterator _subformula )

inlineprotectedinherited

Stores an infeasible subset consisting only of the given received formula.

Definition at line 920 of file Module.h.

◆ receivedVariable()

bool smtrat::Module::receivedVariable ( carl::Variable::Arg _var ) const

inlineinherited

Definition at line 377 of file Module.h.

◆ reduceDB()

template<class Settings >

void smtrat::SATModule< Settings >::reduceDB ( )

private

reduceDB : () -> [void]

Description: Remove half of the learnt clauses, minus the clauses locked by the current assignment. Locked clauses are clauses that are reason to some assignment. Binary clauses are never removed.

◆ relocAll()

template<class Settings >

void smtrat::SATModule< Settings >::relocAll ( Minisat::ClauseAllocator & to )

private

[Minisat related code]

Parameters

to	[Minisat related code]

◆ remove()

void smtrat::Module::remove ( ModuleInput::const_iterator _subformula )

virtualinherited

Removes everything related to the given sub-formula of the received formula.

However, it is desired not to lose track of search spaces where no satisfying assignment can be found for the remaining sub-formulas.

Parameters

_subformula The sub formula of the received formula to remove.

Reimplemented in smtrat::PModule.

Definition at line 159 of file Module.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ removeClause()

template<class Settings >

void smtrat::SATModule< Settings >::removeClause ( Minisat::CRef cr )

private

Detach and free a clause.

Parameters

cr	[Minisat related code]

◆ removeCore() [1/2]

virtual void smtrat::Module::removeCore ( [[maybe_unused] ] ModuleInput::const_iterator formula )

inlineprotectedvirtualinherited

Removes everything related to the given sub-formula of the received formula.

However, it is desired not to lose track of search spaces where no satisfying assignment can be found for the remaining sub-formulas.

Parameters

formula The sub formula of the received formula to remove.

Definition at line 729 of file Module.h.

Here is the caller graph for this function:

◆ removeCore() [2/2]

template<class Settings >

void smtrat::SATModule< Settings >::removeCore ( ModuleInput::const_iterator )

Removes everything related to the given sub-formula of the received formula.

Parameters

_subformula The sub formula of the received formula to remove.

◆ removeLiteralOrigin()

template<class Settings >

void smtrat::SATModule< Settings >::removeLiteralOrigin	(	Minisat::Lit	_litToRemove,
		const FormulaT &	_origin
	)

private

◆ removeOrigin()

std::pair<ModuleInput::iterator,bool> smtrat::Module::removeOrigin	(	ModuleInput::iterator	_formula,
		const FormulaT &	_origin
	)

inlineprotectedinherited

Definition at line 814 of file Module.h.

Here is the call graph for this function:

◆ removeOrigins()

std::pair<ModuleInput::iterator,bool> smtrat::Module::removeOrigins	(	ModuleInput::iterator	_formula,
		const std::shared_ptr< std::vector< FormulaT >> &	_origins
	)

inlineprotectedinherited

Definition at line 823 of file Module.h.

Here is the call graph for this function:

◆ removeSatisfied()

template<class Settings >

void smtrat::SATModule< Settings >::removeSatisfied ( Minisat::vec< Minisat::CRef > & cs )

private

Removes all satisfied clauses from the given vector of clauses, which should only be performed in decision level 0.

Parameters

cs	The vector of clauses wherein to remove all satisfied clauses.

◆ removeTheoryPropagation()

template<class Settings >

void smtrat::SATModule< Settings >::removeTheoryPropagation ( int _position )

private

◆ removeUpperBoundOnMinimal()

template<class Settings >

void smtrat::SATModule< Settings >::removeUpperBoundOnMinimal ( )

◆ resetVariableAssignment()

template<class Settings >

void smtrat::SATModule< Settings >::resetVariableAssignment ( Minisat::Var _var )

private

◆ rPassedFormula()

const ModuleInput& smtrat::Module::rPassedFormula ( ) const

inlineinherited

Returns: A reference to the formula passed to the backends of this module.

Definition at line 455 of file Module.h.

Here is the caller graph for this function:

◆ rReceivedFormula()

const ModuleInput& smtrat::Module::rReceivedFormula ( ) const

inlineinherited

Returns: A reference to the formula passed to this module.

Definition at line 439 of file Module.h.

Here is the caller graph for this function:

◆ runBackends() [1/2]

virtual Answer smtrat::Module::runBackends ( )

inlineprotectedvirtualinherited

Reimplemented in smtrat::PModule.

Definition at line 1012 of file Module.h.

Here is the caller graph for this function:

◆ runBackends() [2/2]

Answer smtrat::Module::runBackends	(	bool	_final,
		bool	_full,
		carl::Variable	_objective
	)

protectedvirtualinherited

Runs the backend solvers on the passed formula.

Parameters

_final	true, if this satisfiability check will be the last one (for a global sat-check), if its result is SAT
_full	false, if this module should avoid too expensive procedures and rather return unknown instead.
_objective	if not set to NO_VARIABLE, the module should find an assignment minimizing this objective variable; otherwise any assignment is good.

Returns: True, if the passed formula is consistent; False, if the passed formula is inconsistent; Unknown, otherwise.

Reimplemented in smtrat::PModule.

Definition at line 727 of file Module.cpp.

Here is the call graph for this function:

◆ satisfied()

template<class Settings >

bool smtrat::SATModule< Settings >::satisfied ( const Minisat::Clause & c ) const

private

Parameters

c	[Minisat related code]

Returns: TRUE if a clause is satisfied in the current state.

◆ search()

template<class Settings >

Minisat::lbool smtrat::SATModule< Settings >::search ( int nof_conflicts = 100 )

private

search : (nof_conflicts : int) (params : const SearchParams&) -> [lbool]

Description: Search for a model the specified number of conflicts. NOTE! Use negative value for 'nof_conflicts' indicate infinity.

Output: 'l_True' if a partial assignment that is consistent with respect to the clause set is found. If all variables are decision variables, this means that the clause set is satisfiable. 'l_False' if the clause set is unsatisfiable. 'l_Undef' if the bound on number of conflicts is reached.

Parameters

nof_conflicts The number of conflicts after which a restart is forced.

Returns: l_True, if the considered clauses are satisfiable; l_False, if the considered clauses are unsatisfiable; l_Undef, if it could not been detected whether the given set of clauses is satisfiable or not.

◆ setConfBudget()

template<class Settings >

void smtrat::SATModule< Settings >::setConfBudget ( int64_t x )

inlineprivate

[Minisat related code]

Parameters

x	[Minisat related code]

Definition at line 1085 of file SATModule.h.

◆ setDecisionVar()

template<class Settings >

void smtrat::SATModule< Settings >::setDecisionVar	(	Minisat::Var	v,
		bool	b,
		bool	insertIntoHeap = `true`
	)

inlineprivate

Declare if a variable should be eligible for selection in the decision heuristic.

Parameters

v	The variable to change the eligibility for selection in the decision heuristic.
b	true, if the variable should be eligible for selection in the decision heuristic.

Definition at line 909 of file SATModule.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ setId()

void smtrat::Module::setId ( std::size_t _id )

inlineinherited

Sets this modules unique ID to identify itself.

Parameters

_id	The id to set this module's id to.

Definition at line 405 of file Module.h.

Here is the caller graph for this function:

◆ setPolarity()

template<class Settings >

void smtrat::SATModule< Settings >::setPolarity	(	Minisat::Var	v,
		bool	b
	)

inlineprivate

Declare which polarity the decision heuristic should use for a variable.

Requires mode 'polarity_user'.

Parameters

v	The variable to set the polarity for.
b	true, if the variables should be preferably assigned to false.

Definition at line 899 of file SATModule.h.

◆ setPropBudget()

template<class Settings >

void smtrat::SATModule< Settings >::setPropBudget ( int64_t x )

inlineprivate

[Minisat related code]

Parameters

x	[Minisat related code]

Definition at line 1094 of file SATModule.h.

◆ setThreadPriority()

void smtrat::Module::setThreadPriority ( thread_priority _threadPriority )

inlineinherited

Sets the priority of this module to get a thread for running its check procedure.

Parameters

_threadPriority The priority to set this module's thread priority to.

Definition at line 423 of file Module.h.

Here is the caller graph for this function:

◆ simplify()

template<class Settings >

void smtrat::SATModule< Settings >::simplify ( )

private

Removes already satisfied clauses and performs simplifications on all clauses.

◆ solverState()

Answer smtrat::Module::solverState ( ) const

inlineinherited

Returns: True, if this module is in a state, such that it has found a solution for its received formula; False, if this module is in a state, such that it has determined that there is no solution for its received formula; Unknown, otherwise.

Definition at line 388 of file Module.h.

Here is the caller graph for this function:

◆ splitUnequalConstraint()

void smtrat::Module::splitUnequalConstraint ( const FormulaT & _unequalConstraint )

protectedinherited

Adds the following lemmas for the given constraint p!=0.

 (p!=0 <-> (p<0 or p>0))

and not(p<0 and p>0)

Parameters

_unequalConstraint A constraint having the relation symbol !=.

Definition at line 565 of file Module.cpp.

◆ storeLemmas()

template<class Settings >

Minisat::CRef smtrat::SATModule< Settings >::storeLemmas ( )

private

Here is the caller graph for this function:

◆ supportedConstraintType()

template<class Settings >

bool smtrat::SATModule< Settings >::supportedConstraintType ( const FormulaT & _formula ) const

inlineprivate

Definition at line 1703 of file SATModule.h.

◆ theory_level()

template<class Settings >

int smtrat::SATModule< Settings >::theory_level ( Minisat::Var x ) const

inlineprivate

Definition at line 1615 of file SATModule.h.

Here is the call graph for this function:

◆ theoryCall()

template<class Settings >

void smtrat::SATModule< Settings >::theoryCall ( )

private

◆ theoryValue() [1/2]

template<class Settings >

Minisat::lbool smtrat::SATModule< Settings >::theoryValue ( Minisat::Lit p ) const

inlineprivate

Definition at line 1035 of file SATModule.h.

Here is the call graph for this function:

◆ theoryValue() [2/2]

template<class Settings >

Minisat::lbool smtrat::SATModule< Settings >::theoryValue ( Minisat::Var x ) const

inlineprivate

Definition at line 936 of file SATModule.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ threadPriority()

thread_priority smtrat::Module::threadPriority ( ) const

inlineinherited

Returns: The priority of this module to get a thread for running its check procedure.

Definition at line 414 of file Module.h.

Here is the caller graph for this function:

◆ trailIndex()

template<class Settings >

int smtrat::SATModule< Settings >::trailIndex ( Minisat::Var _var ) const

inlineprivate

Definition at line 1631 of file SATModule.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ uncheckedEnqueue()

template<class Settings >

void smtrat::SATModule< Settings >::uncheckedEnqueue	(	Minisat::Lit	p,
		Minisat::CRef	from = `Minisat::CRef_Undef`
	)

private

Enqueue a literal.

Assumes value of literal is undefined.

Parameters

p	The literal to enqueue. (The variable in the literal is set to true, if the literal is positive, and to false, if the literal is negative).s
from	A reference to the clause, which implied this assignment.

Here is the caller graph for this function:

◆ updateAllModels()

template<class Settings >

void smtrat::SATModule< Settings >::updateAllModels ( )

virtual

Updates all satisfying models, if the solver has detected the consistency of the received formula, beforehand.

Reimplemented from smtrat::Module.

◆ updateCNFInfoCounter()

template<class Settings >

void smtrat::SATModule< Settings >::updateCNFInfoCounter	(	typename FormulaCNFInfosMap::iterator	_iter,
		const FormulaT &	_origin,
		bool	_increment
	)

private

◆ updateInfeasibleSubset()

template<class Settings >

void smtrat::SATModule< Settings >::updateInfeasibleSubset ( )

Updates the infeasible subset found by the SATModule, if the received formula is unsatisfiable.

◆ updateLemmas()

void smtrat::Module::updateLemmas ( )

inherited

Stores all lemmas of any backend of this module in its own lemma vector.

Definition at line 919 of file Module.cpp.

Here is the caller graph for this function:

◆ updateModel() [1/2]

template<class Settings >

void smtrat::SATModule< Settings >::updateModel ( ) const

virtual

Updates the model, if the solver has detected the consistency of the received formula, beforehand.

Reimplemented from smtrat::Module.

◆ updateModel() [2/2]

template<class Settings >

void smtrat::SATModule< Settings >::updateModel	(	Model &	model,
		bool	only_relevant_variables = `false`
	)		const

private

Updates the model, if the solver has detected the consistency of the received formula, beforehand.

Parameters

model	The model to update with the current assignment
only_relevant_variables	If true, only variables in mRelevantVariables are part of the model

◆ usedBackends()

const std::vector<Module*>& smtrat::Module::usedBackends ( ) const

inlineinherited

Returns: The backends of this module which are currently used (conditions to use this module are fulfilled for the passed formula).

Definition at line 488 of file Module.h.

Here is the caller graph for this function:

◆ value() [1/2]

template<class Settings >

Minisat::lbool smtrat::SATModule< Settings >::value ( Minisat::Lit p ) const

inlineprivate

Parameters

p	The literal to get its value for.

Returns: The current value of a literal.

Definition at line 1031 of file SATModule.h.

Here is the call graph for this function:

◆ value() [2/2]

template<class Settings >

Minisat::lbool smtrat::SATModule< Settings >::value ( Minisat::Var x ) const

inlineprivate

Parameters

x	The variable to get its value for.

Returns: The current value of a variable.

Definition at line 928 of file SATModule.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ varBumpActivity() [1/2]

template<class Settings >

void smtrat::SATModule< Settings >::varBumpActivity ( Minisat::Var v )

inlineprivate

Increase a variable with the current 'bump' value.

Parameters

v	[Minisat related code]

Definition at line 1475 of file SATModule.h.

Here is the call graph for this function:

◆ varBumpActivity() [2/2]

template<class Settings >

void smtrat::SATModule< Settings >::varBumpActivity	(	Minisat::Var	v,
		double	inc
	)

inlineprivate

Increase a variable with the current 'bump' value.

Parameters

v	[Minisat related code]
inc	[Minisat related code]

Definition at line 1436 of file SATModule.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ varDecayActivity()

template<class Settings >

void smtrat::SATModule< Settings >::varDecayActivity ( )

inlineprivate

Decay all variables with the specified factor.

Implemented by increasing the 'bump' value instead.

Definition at line 1426 of file SATModule.h.

◆ withinBudget()

template<class Settings >

bool smtrat::SATModule< Settings >::withinBudget ( ) const

inlineprivate

Returns: [Minisat related code]

Definition at line 1655 of file SATModule.h.

Friends And Related Function Documentation

◆ VarSchedulerBase

template<class Settings >

friend class VarSchedulerBase

friend

Definition at line 68 of file SATModule.h.

◆ VarSchedulerMcsatBase

template<class Settings >

friend class VarSchedulerMcsatBase

friend

Definition at line 69 of file SATModule.h.

Field Documentation

◆ activity

template<class Settings >

Minisat::vec<double> smtrat::SATModule< Settings >::activity

private

A heuristic measurement of the activity of a variable.

Definition at line 471 of file SATModule.h.

◆ add_tmp

template<class Settings >

Minisat::vec<Minisat::Lit> smtrat::SATModule< Settings >::add_tmp

private

[Minisat related code]

Definition at line 513 of file SATModule.h.

◆ analyze_stack

template<class Settings >

Minisat::vec<Minisat::Lit> smtrat::SATModule< Settings >::analyze_stack

private

[Minisat related code]

Definition at line 509 of file SATModule.h.

◆ analyze_toclear

template<class Settings >

Minisat::vec<Minisat::Lit> smtrat::SATModule< Settings >::analyze_toclear

private

[Minisat related code]

Definition at line 511 of file SATModule.h.

◆ assigns

template<class Settings >

Minisat::vec<Minisat::lbool> smtrat::SATModule< Settings >::assigns

private

The current assignments.

Definition at line 477 of file SATModule.h.

◆ assumptions

template<class Settings >

Minisat::vec<Minisat::Lit> smtrat::SATModule< Settings >::assumptions

private

Current set of assumptions provided to solve by the user.

Definition at line 495 of file SATModule.h.

◆ asynch_interrupt

template<class Settings >

bool smtrat::SATModule< Settings >::asynch_interrupt

private

[Minisat related code]

Definition at line 527 of file SATModule.h.

◆ ca

template<class Settings >

Minisat::ClauseAllocator smtrat::SATModule< Settings >::ca

private

[Minisat related code]

Definition at line 503 of file SATModule.h.

◆ ccmin_mode

template<class Settings >

int smtrat::SATModule< Settings >::ccmin_mode

private

Controls conflict clause minimization (0=none, 1=basic, 2=deep).

Definition at line 429 of file SATModule.h.

◆ cla_inc

template<class Settings >

double smtrat::SATModule< Settings >::cla_inc

private

Amount to bump next clause with.

Definition at line 469 of file SATModule.h.

◆ clause_decay

template<class Settings >

double smtrat::SATModule< Settings >::clause_decay

private

[Minisat related code]

Definition at line 421 of file SATModule.h.

◆ clauses

template<class Settings >

Minisat::vec<Minisat::CRef> smtrat::SATModule< Settings >::clauses

private

List of problem clauses.

Definition at line 461 of file SATModule.h.

◆ clauses_literals

template<class Settings >

uint64_t smtrat::SATModule< Settings >::clauses_literals

private

Definition at line 455 of file SATModule.h.

◆ conflict_budget

template<class Settings >

int64_t smtrat::SATModule< Settings >::conflict_budget

private

-1 means no budget.

Definition at line 523 of file SATModule.h.

◆ conflicts

template<class Settings >

uint64_t smtrat::SATModule< Settings >::conflicts

private

Definition at line 453 of file SATModule.h.

◆ dec_vars

template<class Settings >

uint64_t smtrat::SATModule< Settings >::dec_vars

private

[Minisat related code]

Definition at line 455 of file SATModule.h.

◆ decision

template<class Settings >

Minisat::vec<char> smtrat::SATModule< Settings >::decision

private

Declares if a variable is eligible for selection in the decision heuristic.

Definition at line 481 of file SATModule.h.

◆ decisions

template<class Settings >

uint64_t smtrat::SATModule< Settings >::decisions

private

Definition at line 453 of file SATModule.h.

◆ garbage_frac

template<class Settings >

double smtrat::SATModule< Settings >::garbage_frac

private

The fraction of wasted memory allowed before a garbage collection is triggered.

Definition at line 437 of file SATModule.h.

◆ learnt_clause

template<class Settings >

Minisat::vec<Minisat::Lit> smtrat::SATModule< Settings >::learnt_clause

private

For temporary usage.

Definition at line 529 of file SATModule.h.

◆ learnts

template<class Settings >

Minisat::vec<Minisat::CRef> smtrat::SATModule< Settings >::learnts

private

List of learned clauses.

Definition at line 465 of file SATModule.h.

◆ learnts_literals

template<class Settings >

uint64_t smtrat::SATModule< Settings >::learnts_literals

private

Definition at line 455 of file SATModule.h.

◆ learntsize_adjust_cnt

template<class Settings >

int smtrat::SATModule< Settings >::learntsize_adjust_cnt

private

[Minisat related code]

Definition at line 519 of file SATModule.h.

◆ learntsize_adjust_confl

template<class Settings >

double smtrat::SATModule< Settings >::learntsize_adjust_confl

private

[Minisat related code]

Definition at line 517 of file SATModule.h.

◆ learntsize_adjust_inc

template<class Settings >

double smtrat::SATModule< Settings >::learntsize_adjust_inc

private

[Minisat related code]

Definition at line 449 of file SATModule.h.

◆ learntsize_adjust_start_confl

template<class Settings >

int smtrat::SATModule< Settings >::learntsize_adjust_start_confl

private

[Minisat related code]

Definition at line 447 of file SATModule.h.

◆ learntsize_factor

template<class Settings >

double smtrat::SATModule< Settings >::learntsize_factor

private

The initial limit for learned clauses is a factor of the original clauses.(default 1 / 3)

Definition at line 443 of file SATModule.h.

◆ learntsize_inc

template<class Settings >

double smtrat::SATModule< Settings >::learntsize_inc

private

The limit for learned clauses is multiplied with this factor each restart.(default 1.1)

Definition at line 445 of file SATModule.h.

◆ luby_restart

template<class Settings >

bool smtrat::SATModule< Settings >::luby_restart

private

[Minisat related code]

Definition at line 427 of file SATModule.h.

◆ mAllActivitiesChanged

template<class Settings >

bool smtrat::SATModule< Settings >::mAllActivitiesChanged

private

Is true, if we have to communicate all activities to the backends. (This might be the case after rescaling the activities.)

Definition at line 588 of file SATModule.h.

◆ mAllBackends

std::vector<Module*> smtrat::Module::mAllBackends

protectedinherited

The backends of this module which have been used.

Definition at line 227 of file Module.h.

◆ mAllModels

std::vector<Model> smtrat::Module::mAllModels

mutableprotectedinherited

Stores all satisfying assignments.

Definition at line 201 of file Module.h.

◆ Manager

friend smtrat::Module::Manager

privateinherited

Definition at line 71 of file Module.h.

◆ mAssumedTseitinVariable

template<class Settings >

carl::Bitset smtrat::SATModule< Settings >::mAssumedTseitinVariable

private

Stores whether a given tseitin variable was already added to the assumptions.

Definition at line 605 of file SATModule.h.

◆ max_learnts

template<class Settings >

double smtrat::SATModule< Settings >::max_learnts

private

[Minisat related code]

Definition at line 515 of file SATModule.h.

◆ max_literals

template<class Settings >

uint64_t smtrat::SATModule< Settings >::max_literals

private

Definition at line 455 of file SATModule.h.

◆ mBackendsFoundAnswer

std::atomic_bool* smtrat::Module::mBackendsFoundAnswer

protectedinherited

This flag is passed to any backend and if it determines an answer to a prior check call, this flag is fired.

Definition at line 220 of file Module.h.

◆ mBooleanConstraintMap

template<class Settings >

BooleanConstraintMap smtrat::SATModule< Settings >::mBooleanConstraintMap

private

Maps each Minisat variable to a pair of Abstractions, one contains the abstraction information of the literal being the variable and one contains the abstraction information of the literal being the variables negation.

Definition at line 563 of file SATModule.h.

◆ mBooleanVarMap

template<class Settings >

BooleanVarMap smtrat::SATModule< Settings >::mBooleanVarMap

private

Maps the Boolean variables to their corresponding Minisat variable.

Definition at line 570 of file SATModule.h.

◆ mBusy

template<class Settings >

bool smtrat::SATModule< Settings >::mBusy

private

Definition at line 543 of file SATModule.h.

◆ mChangedActivities

template<class Settings >

std::vector<signed> smtrat::SATModule< Settings >::mChangedActivities

private

Stores all clauses in which the activities have been changed.

Definition at line 590 of file SATModule.h.

◆ mChangedBooleans

template<class Settings >

std::vector<signed> smtrat::SATModule< Settings >::mChangedBooleans

private

Stores all Literals for which the abstraction information might be changed.

Definition at line 586 of file SATModule.h.

◆ mChangedPassedFormula

template<class Settings >

bool smtrat::SATModule< Settings >::mChangedPassedFormula

private

A flag, which is set to true, if anything has been changed in the passed formula between now and the last consistency check.

Definition at line 535 of file SATModule.h.

◆ mClauseInformation

template<class Settings >

carl::FastMap<Minisat::CRef,ClauseInformation> smtrat::SATModule< Settings >::mClauseInformation

private

Definition at line 580 of file SATModule.h.

◆ mComputeAllSAT

template<class Settings >

bool smtrat::SATModule< Settings >::mComputeAllSAT

private

A flag, which is set to true, if all satisfying assignments should be computed.

Definition at line 537 of file SATModule.h.

◆ mConstraintLiteralMap

template<class Settings >

ConstraintLiteralsMap smtrat::SATModule< Settings >::mConstraintLiteralMap

private

Maps the constraints occurring in the SAT module to their abstractions.

We store a vector of literals for each constraints, which is only used in the optimization, which applies valid substitutions.

Definition at line 568 of file SATModule.h.

◆ mConstraintsToInform

carl::FastSet<FormulaT> smtrat::Module::mConstraintsToInform

protectedinherited

Stores the constraints which the backends must be informed about.

Definition at line 233 of file Module.h.

◆ mCurr_Restarts

template<class Settings >

int smtrat::SATModule< Settings >::mCurr_Restarts

private

The number of restarts made.

Definition at line 554 of file SATModule.h.

◆ mCurrentAssignmentConsistent

template<class Settings >

Answer smtrat::SATModule< Settings >::mCurrentAssignmentConsistent

private

Stores gained information about the current assignment's consistency.

If we know from the last consistency check, whether the current assignment is consistent, this member is SAT, if we know that it is inconsistent it is UNSAT, otherwise Unknown.

Definition at line 550 of file SATModule.h.

◆ mCurrentTheoryConflictEvaluations

template<class Settings >

std::map<std::pair<size_t,size_t>,size_t> smtrat::SATModule< Settings >::mCurrentTheoryConflictEvaluations

private

Definition at line 614 of file SATModule.h.

◆ mCurrentTheoryConflicts

template<class Settings >

std::vector<Minisat::vec<Minisat::Lit> > smtrat::SATModule< Settings >::mCurrentTheoryConflicts

private

Definition at line 610 of file SATModule.h.

◆ mCurrentTheoryConflictTypes

template<class Settings >

std::vector<unsigned> smtrat::SATModule< Settings >::mCurrentTheoryConflictTypes

private

Definition at line 612 of file SATModule.h.

◆ mExcludedAssignments

template<class Settings >

bool smtrat::SATModule< Settings >::mExcludedAssignments

private

Definition at line 545 of file SATModule.h.

◆ mFinalCheck

bool smtrat::Module::mFinalCheck

protectedinherited

true, if the check procedure should perform a final check which especially means not to postpone splitting decisions

Definition at line 205 of file Module.h.

◆ mFirstPosInLastBranches

std::size_t smtrat::Module::mFirstPosInLastBranches = 0

staticinherited

The beginning of the cyclic buffer storing the last branches.

Definition at line 275 of file Module.h.

◆ mFirstSubformulaToPass

ModuleInput::iterator smtrat::Module::mFirstSubformulaToPass

protectedinherited

Stores the position of the first sub-formula in the passed formula, which has not yet been considered for a consistency check of the backends.

Definition at line 231 of file Module.h.

◆ mFirstUncheckedReceivedSubformula

ModuleInput::const_iterator smtrat::Module::mFirstUncheckedReceivedSubformula

protectedinherited

Stores the position of the first (by this module) unchecked sub-formula of the received formula.

Definition at line 237 of file Module.h.

◆ mFormulaAssumptionMap

template<class Settings >

carl::FastMap<FormulaT, Minisat::Lit> smtrat::SATModule< Settings >::mFormulaAssumptionMap

private

Definition at line 574 of file SATModule.h.

◆ mFormulaCNFInfosMap

template<class Settings >

FormulaCNFInfosMap smtrat::SATModule< Settings >::mFormulaCNFInfosMap

private

Maps the clauses in the received formula to the corresponding Minisat clause and Minisat literal.

Definition at line 576 of file SATModule.h.

◆ mFoundAnswer

Conditionals smtrat::Module::mFoundAnswer

protectedinherited

Vector of Booleans: If any of them is true, we have to terminate a running check procedure.

Definition at line 223 of file Module.h.

◆ mFullAssignmentCheckedForConsistency

template<class Settings >

bool smtrat::SATModule< Settings >::mFullAssignmentCheckedForConsistency

private

Definition at line 539 of file SATModule.h.

◆ mFullCheck

bool smtrat::Module::mFullCheck

protectedinherited

false, if this module should avoid too expensive procedures and rather return unknown instead.

Definition at line 207 of file Module.h.

◆ mFutureChangedBooleans

template<class Settings >

std::map<carl::Variable, std::vector<signed> > smtrat::SATModule< Settings >::mFutureChangedBooleans

private

Definition at line 638 of file SATModule.h.

◆ mId

std::size_t smtrat::Module::mId

privateinherited

A unique ID to identify this module instance. (Could be useful but currently nowhere used)

Definition at line 184 of file Module.h.

◆ mInfeasibleSubsets

std::vector<FormulaSetT> smtrat::Module::mInfeasibleSubsets

protectedinherited

Stores the infeasible subsets.

Definition at line 195 of file Module.h.

◆ mInformedConstraints

carl::FastSet<FormulaT> smtrat::Module::mInformedConstraints

protectedinherited

Stores the position of the first constraint of which no backend has been informed about.

Definition at line 235 of file Module.h.

◆ mLastBranches

std::vector< Branching > smtrat::Module::mLastBranches = std::vector<Branching>(mNumOfBranchVarsToStore, Branching(typename Poly::PolyType(), 0))

staticinherited

Stores the last branches in a cycle buffer.

Definition at line 273 of file Module.h.

◆ mLearntDeductions

template<class Settings >

ClauseSet smtrat::SATModule< Settings >::mLearntDeductions

private

If problem is unsatisfiable (possibly under assumptions), this vector represent the final conflict clause expressed in the assumptions.

Definition at line 578 of file SATModule.h.

◆ mLemmas

template<class Settings >

Minisat::vec<Minisat::vec<Minisat::Lit> > smtrat::SATModule< Settings >::mLemmas

private

literals propagated by lemmas

Definition at line 628 of file SATModule.h.

◆ mLemmasRemovable

template<class Settings >

Minisat::vec<bool> smtrat::SATModule< Settings >::mLemmasRemovable

private

is the lemma removable

Definition at line 630 of file SATModule.h.

◆ mLevelCounter

template<class Settings >

std::unordered_set<int> smtrat::SATModule< Settings >::mLevelCounter

private

Definition at line 616 of file SATModule.h.

◆ mLiteralClausesMap

template<class Settings >

std::unordered_map<int,std::unordered_set<Minisat::CRef> > smtrat::SATModule< Settings >::mLiteralClausesMap

private

Definition at line 582 of file SATModule.h.

◆ mLiteralsActivOccurrences

template<class Settings >

std::vector<std::pair<size_t,size_t> > smtrat::SATModule< Settings >::mLiteralsActivOccurrences

private

Definition at line 624 of file SATModule.h.

◆ mLiteralsClausesMap

template<class Settings >

std::vector<LiteralClauses> smtrat::SATModule< Settings >::mLiteralsClausesMap

private

Definition at line 622 of file SATModule.h.

◆ mMCSAT

template<class Settings >

mcsat::MCSATMixin<typename Settings::MCSATSettings> smtrat::SATModule< Settings >::mMCSAT

private

Definition at line 637 of file SATModule.h.

◆ mMinisatVarMap

template<class Settings >

MinisatVarMap smtrat::SATModule< Settings >::mMinisatVarMap

private

Maps the Minisat variables to their corresponding boolean variable.

Definition at line 572 of file SATModule.h.

◆ mModel

Model smtrat::Module::mModel

mutableprotectedinherited

Stores the assignment of the current satisfiable result, if existent.

Definition at line 199 of file Module.h.

◆ mModelComputed

bool smtrat::Module::mModelComputed

mutableprotectedinherited

True, if the model has already been computed.

Definition at line 203 of file Module.h.

◆ mModuleName

std::string smtrat::Module::mModuleName

privateinherited

Definition at line 191 of file Module.h.

◆ mNonassumedTseitinVariable

template<class Settings >

carl::Bitset smtrat::SATModule< Settings >::mNonassumedTseitinVariable

private

Stores whether a given tseitin variable was not yet added to the assumptions, but represents a top-level clause.

Tseitin variables for top-level clauses are only assumed lazily if they occur in another clause.

Definition at line 608 of file SATModule.h.

◆ mNonTseitinShadowedOccurrences

template<class Settings >

Minisat::vec<unsigned> smtrat::SATModule< Settings >::mNonTseitinShadowedOccurrences

private

Definition at line 597 of file SATModule.h.

◆ mNumberOfFullLazyCalls

template<class Settings >

size_t smtrat::SATModule< Settings >::mNumberOfFullLazyCalls

private

The number of full laze calls made.

Definition at line 552 of file SATModule.h.

◆ mNumberOfSatisfiedClauses

template<class Settings >

size_t smtrat::SATModule< Settings >::mNumberOfSatisfiedClauses

private

Definition at line 584 of file SATModule.h.

◆ mNumberOfTheoryCalls

template<class Settings >

unsigned smtrat::SATModule< Settings >::mNumberOfTheoryCalls

private

The number of theory calls made.

Definition at line 556 of file SATModule.h.

◆ mNumOfBranchVarsToStore

std::size_t smtrat::Module::mNumOfBranchVarsToStore = 5

staticinherited

The number of different variables to consider for a probable infinite loop of branchings.

Definition at line 271 of file Module.h.

◆ mObjectiveVariable

carl::Variable smtrat::Module::mObjectiveVariable

protectedinherited

Objective variable to be minimized. If set to NO_VARIABLE, a normal sat check should be performed.

Definition at line 209 of file Module.h.

◆ mOldSplittingVariables

std::vector< FormulaT > smtrat::Module::mOldSplittingVariables

staticinherited

Reusable splitting variables.

Definition at line 277 of file Module.h.

◆ mOptimumComputed

template<class Settings >

bool smtrat::SATModule< Settings >::mOptimumComputed

private

Definition at line 541 of file SATModule.h.

◆ mpManager

Manager* const smtrat::Module::mpManager

protectedinherited

A reference to the manager.

Definition at line 197 of file Module.h.

◆ mpPassedFormula

ModuleInput* smtrat::Module::mpPassedFormula

privateinherited

The formula passed to the backends of this module.

Definition at line 190 of file Module.h.

◆ mpReceivedFormula

const ModuleInput* smtrat::Module::mpReceivedFormula

privateinherited

The formula passed to this module.

Definition at line 188 of file Module.h.

◆ mPropagatedLemmas

template<class Settings >

VarLemmaMap smtrat::SATModule< Settings >::mPropagatedLemmas

private

Stores for each variable the corresponding formulas which control its value.

Definition at line 593 of file SATModule.h.

◆ mPropagationFreeDecisions

template<class Settings >

std::vector<Minisat::Lit> smtrat::SATModule< Settings >::mPropagationFreeDecisions

private

Definition at line 626 of file SATModule.h.

◆ mReceivedFormulaPurelyPropositional

template<class Settings >

bool smtrat::SATModule< Settings >::mReceivedFormulaPurelyPropositional

private

Definition at line 558 of file SATModule.h.

◆ mRelevantVariables

template<class Settings >

std::vector<int> smtrat::SATModule< Settings >::mRelevantVariables

private

Stores Minisat indexes of all relevant variables.

Definition at line 595 of file SATModule.h.

◆ mSmallerMusesCheckCounter

unsigned smtrat::Module::mSmallerMusesCheckCounter

mutableprotectedinherited

Counter used for the generation of the smt2 files to check for smaller muses.

Definition at line 239 of file Module.h.

◆ mSolverState

std::atomic<Answer> smtrat::Module::mSolverState

protectedinherited

States whether the received formula is known to be satisfiable or unsatisfiable otherwise it is set to unknown.

Definition at line 215 of file Module.h.

◆ mStatistics

ModuleStatistics& smtrat::Module::mStatistics = statistics_get<ModuleStatistics>(moduleName())

privateinherited

Definition at line 192 of file Module.h.

◆ mTheoryConflictIdCounter

template<class Settings >

size_t smtrat::SATModule< Settings >::mTheoryConflictIdCounter

private

Definition at line 618 of file SATModule.h.

◆ mTheoryPropagations

std::vector<TheoryPropagation> smtrat::Module::mTheoryPropagations

protectedinherited

Definition at line 211 of file Module.h.

◆ mThreadPriority

thread_priority smtrat::Module::mThreadPriority

privateinherited

The priority of this module to get a thread for running its check procedure.

Definition at line 186 of file Module.h.

◆ mTrueVar

template<class Settings >

Minisat::Var smtrat::SATModule< Settings >::mTrueVar

private

Variable representing true.

Definition at line 531 of file SATModule.h.

◆ mTseitinVarFormulaMap

template<class Settings >

carl::FastMap<int, FormulaT> smtrat::SATModule< Settings >::mTseitinVarFormulaMap

private

Definition at line 601 of file SATModule.h.

◆ mTseitinVariable

template<class Settings >

carl::Bitset smtrat::SATModule< Settings >::mTseitinVariable

private

Stores whether a given variable is a tseitin variable.

Definition at line 603 of file SATModule.h.

◆ mTseitinVarShadows

template<class Settings >

TseitinVarShadows smtrat::SATModule< Settings >::mTseitinVarShadows

private

Definition at line 599 of file SATModule.h.

◆ mUnorderedClauseLookup

template<class Settings >

UnorderedClauseLookup smtrat::SATModule< Settings >::mUnorderedClauseLookup

private

Definition at line 670 of file SATModule.h.

◆ mUpperBoundOnMinimal

template<class Settings >

ModuleInput::iterator smtrat::SATModule< Settings >::mUpperBoundOnMinimal

private

Definition at line 620 of file SATModule.h.

◆ mUsedBackends

std::vector<Module*> smtrat::Module::mUsedBackends

protectedinherited

The backends of this module which are currently used (conditions to use this module are fulfilled for the passed formula).

Definition at line 225 of file Module.h.

◆ mVariableCounters

std::vector<std::size_t> smtrat::Module::mVariableCounters

protectedinherited

Maps variables to the number of their occurrences.

Definition at line 241 of file Module.h.

◆ ok

template<class Settings >

bool smtrat::SATModule< Settings >::ok

private

If FALSE, the constraints are already unsatisfiable. No part of the solver state may be used!

Definition at line 459 of file SATModule.h.

◆ phase_saving

template<class Settings >

int smtrat::SATModule< Settings >::phase_saving

private

Controls the level of phase saving (0=none, 1=limited, 2=full).

Definition at line 431 of file SATModule.h.

◆ polarity

template<class Settings >

Minisat::vec<char> smtrat::SATModule< Settings >::polarity

private

The preferred polarity of each variable.

Definition at line 479 of file SATModule.h.

◆ progress_estimate

template<class Settings >

double smtrat::SATModule< Settings >::progress_estimate

private

Set by 'search()'.

Definition at line 499 of file SATModule.h.

◆ propagation_budget

template<class Settings >

int64_t smtrat::SATModule< Settings >::propagation_budget

private

-1 means no budget.

Definition at line 525 of file SATModule.h.

◆ propagations

template<class Settings >

uint64_t smtrat::SATModule< Settings >::propagations

private

Definition at line 453 of file SATModule.h.

◆ qhead

template<class Settings >

int smtrat::SATModule< Settings >::qhead

private

Head of queue (as index into the trail – no more explicit propagation queue in MiniSat).

Definition at line 489 of file SATModule.h.

◆ random_seed

template<class Settings >

double smtrat::SATModule< Settings >::random_seed

private

[Minisat related code]

Definition at line 425 of file SATModule.h.

◆ random_var_freq

template<class Settings >

double smtrat::SATModule< Settings >::random_var_freq

private

[Minisat related code]

Definition at line 423 of file SATModule.h.

◆ remove_satisfied

template<class Settings >

bool smtrat::SATModule< Settings >::remove_satisfied

private

Indicates whether possibly inefficient linear scan for satisfied clauses should be performed in 'simplify'.

Definition at line 501 of file SATModule.h.

◆ restart_first

template<class Settings >

int smtrat::SATModule< Settings >::restart_first

private

The initial restart limit. (default 100)

Definition at line 439 of file SATModule.h.

◆ restart_inc

template<class Settings >

double smtrat::SATModule< Settings >::restart_inc

private

The factor with which the restart limit is multiplied in each restart. (default 1.5)

Definition at line 441 of file SATModule.h.

◆ rnd_decisions

template<class Settings >

uint64_t smtrat::SATModule< Settings >::rnd_decisions

private

Definition at line 453 of file SATModule.h.

◆ rnd_init_act

template<class Settings >

bool smtrat::SATModule< Settings >::rnd_init_act

private

Initialize variable activities with a small random value.

Definition at line 435 of file SATModule.h.

◆ rnd_pol

template<class Settings >

bool smtrat::SATModule< Settings >::rnd_pol

private

Use random polarities for branching heuristics.

Definition at line 433 of file SATModule.h.

◆ satisfiedClauses

template<class Settings >

Minisat::vec<Minisat::CRef> smtrat::SATModule< Settings >::satisfiedClauses

private

List of problem clauses.

Definition at line 463 of file SATModule.h.

◆ seen

template<class Settings >

Minisat::vec<char> smtrat::SATModule< Settings >::seen

private

Each variable is prefixed by the method in which it is used, except 'seen' which is used in several places.

Definition at line 507 of file SATModule.h.

◆ simpDB_assigns

template<class Settings >

int smtrat::SATModule< Settings >::simpDB_assigns

private

Number of top-level assignments since last execution of 'simplify()'.

Definition at line 491 of file SATModule.h.

◆ simpDB_props

template<class Settings >

int64_t smtrat::SATModule< Settings >::simpDB_props

private

Remaining number of propagations that must be made before next execution of 'simplify()'.

Definition at line 493 of file SATModule.h.

◆ solves

template<class Settings >

uint64_t smtrat::SATModule< Settings >::solves

private

[Minisat related code]

Definition at line 453 of file SATModule.h.

◆ starts

template<class Settings >

uint64_t smtrat::SATModule< Settings >::starts

private

Definition at line 453 of file SATModule.h.

◆ tot_literals

template<class Settings >

uint64_t smtrat::SATModule< Settings >::tot_literals

private

Definition at line 455 of file SATModule.h.

◆ trail

template<class Settings >

Minisat::vec<Minisat::Lit> smtrat::SATModule< Settings >::trail

private

Assignment stack; stores all assignments made in the order they were made.

Definition at line 483 of file SATModule.h.

◆ trail_lim

template<class Settings >

Minisat::vec<int> smtrat::SATModule< Settings >::trail_lim

private

Separator indices for different decision levels in 'trail'.

Definition at line 485 of file SATModule.h.

◆ unknown_excludes

template<class Settings >

Minisat::vec<Minisat::CRef> smtrat::SATModule< Settings >::unknown_excludes

private

List of clauses which exclude a call resulted in unknown.

Definition at line 467 of file SATModule.h.

◆ var_decay

template<class Settings >

double smtrat::SATModule< Settings >::var_decay

private

[Minisat related code]

Definition at line 419 of file SATModule.h.

◆ var_inc

template<class Settings >

double smtrat::SATModule< Settings >::var_inc

private

Amount to bump next variable with.

Definition at line 473 of file SATModule.h.

◆ var_scheduler

template<class Settings >

VarScheduler smtrat::SATModule< Settings >::var_scheduler

private

A priority queue of variables.

Definition at line 497 of file SATModule.h.

◆ vardata

template<class Settings >

Minisat::vec<VarData> smtrat::SATModule< Settings >::vardata

private

Stores reason and level for each variable.

Definition at line 487 of file SATModule.h.

◆ verbosity

template<class Settings >

int smtrat::SATModule< Settings >::verbosity

private

[Minisat related code]

Definition at line 417 of file SATModule.h.

◆ watches

template<class Settings >

Minisat::OccLists<Minisat::Lit, Minisat::vec<Minisat::Watcher>, WatcherDeleted> smtrat::SATModule< Settings >::watches

private

'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).

Definition at line 475 of file SATModule.h.

The documentation for this class was generated from the following file:

smtrat-modules/SATModule/SATModule.h

Data Structures

Public Types

Public Member Functions

Static Public Member Functions

Static Public Attributes

Protected Member Functions

Static Protected Member Functions

Protected Attributes

Private Types

Private Member Functions

Static Private Member Functions

Private Attributes

Friends

Detailed Description

template<class Settings> class smtrat::SATModule< Settings >

Member Typedef Documentation

◆ BooleanConstraintMap

◆ BooleanVarMap

◆ ClauseSet

◆ ClauseVector

◆ ConstraintLiteralsMap

◆ FormulaCNFInfosMap

◆ MinisatVarMap

◆ SettingsType

◆ TseitinVarShadows

◆ VarLemmaMap

◆ VarScheduler

Member Enumeration Documentation

◆ LemmaType

Constructor & Destructor Documentation

◆ SATModule()

◆ ~SATModule()

Member Function Documentation

◆ abstractLevel()

◆ adaptConflictEvaluation()

◆ adaptPassedFormula() [1/2]

◆ adaptPassedFormula() [2/2]

◆ add()

◆ addBooleanAssignments()

◆ addClause()

◆ addClause_()

◆ addClauseIfNew()

◆ addClauses()

◆ addConstraintToInform()

◆ addConstraintToInform_()

◆ addCore() [1/2]

◆ addCore() [2/2]

◆ addInformationRelevantFormula()

◆ addLemma()

◆ addOrigin()

◆ addReceivedSubformulaToPassedFormula()

◆ addSubformulaToPassedFormula() [1/4]

◆ addSubformulaToPassedFormula() [2/4]

◆ addSubformulaToPassedFormula() [3/4]

◆ addSubformulaToPassedFormula() [4/4]

◆ addXorClauses()

◆ allModels()

◆ analyze()

◆ anAnswerFound()

◆ answerFound()

◆ attachClause()

◆ backendsModel()

◆ bool_satisfied()

◆ bool_value() [1/2]

◆ bool_value() [2/2]

◆ branchAt() [1/4]

◆ branchAt() [2/4]

◆ branchAt() [3/4]

◆ branchAt() [4/4]

◆ budgetOff()

◆ cancelAssignmentUntil()

◆ cancelIncludingLiteral()

◆ cancelUntil()

◆ check()

◆ checkAbstractionsConsistency()

◆ checkCore()

◆ checkFormula()

◆ checkGarbage() [1/2]

◆ checkGarbage() [2/2]

◆ checkInfSubsetForMinimality()

template<class Settings>
class smtrat::SATModule< Settings >