15 #include "booleforce.h" 20 booleforce_set_trace(
false);
25 booleforce_set_trace(
true);
46 int r=booleforce_deref(v);
63 return std::string(
"Booleforce version ")+booleforce_version();
73 for(
unsigned j=0; j<tmp.size(); j++)
74 booleforce_add(tmp[j].dimacs());
86 int result=booleforce_sat();
93 case BOOLEFORCE_UNSATISFIABLE:
94 msg=
"SAT checker: instance is UNSATISFIABLE";
97 case BOOLEFORCE_SATISFIABLE:
98 msg=
"SAT checker: instance is SATISFIABLE";
102 msg=
"SAT checker failed: unknown result";
109 if(
result==BOOLEFORCE_UNSATISFIABLE)
112 return P_UNSATISFIABLE;
115 if(
result==BOOLEFORCE_SATISFIABLE)
118 return P_SATISFIABLE;
128 return booleforce_var_in_core(l.
var_no());
bool is_in_core(literalt l) const
bool process_clause(const bvt &bv, bvt &dest)
filter 'true' from clause, eliminate duplicates, recognise trivially satisfied clauses
#define CHECK_RETURN(CONDITION)
virtual void lcnf(const bvt &bv)
virtual const std::string solver_text()
#define PRECONDITION(CONDITION)
satcheck_booleforce_coret()
virtual tvt l_get(literalt a) const
mstreamt & result() const
mstreamt & status() const
virtual ~satcheck_booleforce_baset()
virtual size_t no_variables() const override
virtual resultt prop_solve()
std::vector< literalt > bvt