SATModule.h File Reference

#include <smtrat-common/smtrat-common.h>
#include "mcsat/MCSATMixin.h"
#include "SATSettings.h"
#include "Vec.h"
#include "Heap.h"
#include "Alg.h"
#include "Options.h"
#include "SolverTypes.h"
#include "Sort.h"
#include <math.h>
#include <smtrat-solver/Module.h>
#include "VarScheduler.h"
#include "mcsat/VarSchedulerMcsat.h"

Include dependency graph for SATModule.h:

Go to the source code of this file.

Data Structures
class	smtrat::SATModule< Settings >
	Implements a module performing DPLL style SAT checking. More...
struct	smtrat::SATModule< Settings >::VarData
	Stores information about a Minisat variable. More...
struct	smtrat::SATModule< Settings >::Abstraction
	Stores all information regarding a Boolean abstraction of a constraint. More...
struct	smtrat::SATModule< Settings >::ClauseInformation
struct	smtrat::SATModule< Settings >::WatcherDeleted
	[Minisat related code] More...
struct	smtrat::SATModule< Settings >::VarOrderLt
struct	smtrat::SATModule< Settings >::CNFInfos
struct	smtrat::SATModule< Settings >::lemma_lt
struct	smtrat::SATModule< Settings >::LiteralClauses
struct	smtrat::SATModule< Settings >::UnorderedClauseLookup
struct	smtrat::SATModule< Settings >::UnorderedClauseLookup::UnorderedClauseHasher

Namespaces
	smtrat
	Class to create the formulas for axioms.

Detailed Description

Author

Florian Corzilius corzi.nosp@m.lius.nosp@m.@cs.r.nosp@m.wth-.nosp@m.aache.nosp@m.n.de

Since

2012-01-18

Version

2014-10-02

Supports optimization.

Definition in file SATModule.h.