54 lines
1.4 KiB
Diff
54 lines
1.4 KiB
Diff
--- src/prop/cryptominisat.cpp.orig 2020-06-19 10:59:27.000000000 -0600
|
|
+++ src/prop/cryptominisat.cpp 2020-06-21 11:51:21.496211208 -0600
|
|
@@ -73,15 +73,8 @@ CryptoMinisatSolver::CryptoMinisatSolver
|
|
|
|
void CryptoMinisatSolver::init()
|
|
{
|
|
- d_true = newVar();
|
|
- d_false = newVar();
|
|
-
|
|
- std::vector<CMSat::Lit> clause(1);
|
|
- clause[0] = CMSat::Lit(d_true, false);
|
|
- d_solver->add_clause(clause);
|
|
-
|
|
- clause[0] = CMSat::Lit(d_false, true);
|
|
- d_solver->add_clause(clause);
|
|
+ d_true = undefSatVariable;
|
|
+ d_false = undefSatVariable;
|
|
}
|
|
|
|
CryptoMinisatSolver::~CryptoMinisatSolver() {}
|
|
@@ -158,10 +151,32 @@ SatVariable CryptoMinisatSolver::newVar
|
|
}
|
|
|
|
SatVariable CryptoMinisatSolver::trueVar() {
|
|
+ if (d_true == undefSatVariable) {
|
|
+ d_true = newVar();
|
|
+ d_false = newVar();
|
|
+
|
|
+ std::vector<CMSat::Lit> clause(1);
|
|
+ clause[0] = CMSat::Lit(d_true, false);
|
|
+ d_solver->add_clause(clause);
|
|
+
|
|
+ clause[0] = CMSat::Lit(d_false, true);
|
|
+ d_solver->add_clause(clause);
|
|
+ }
|
|
return d_true;
|
|
}
|
|
|
|
SatVariable CryptoMinisatSolver::falseVar() {
|
|
+ if (d_true == undefSatVariable) {
|
|
+ d_true = newVar();
|
|
+ d_false = newVar();
|
|
+
|
|
+ std::vector<CMSat::Lit> clause(1);
|
|
+ clause[0] = CMSat::Lit(d_true, false);
|
|
+ d_solver->add_clause(clause);
|
|
+
|
|
+ clause[0] = CMSat::Lit(d_false, true);
|
|
+ d_solver->add_clause(clause);
|
|
+ }
|
|
return d_false;
|
|
}
|
|
|