Fix inadvertent corruption of -flags patch.
This commit is contained in:
parent
eb73525431
commit
bd906d4c2b
|
@ -45,59 +45,6 @@
|
||||||
|
|
||||||
CFLAGS += -I$(MROOT) -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS
|
CFLAGS += -I$(MROOT) -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS
|
||||||
LFLAGS += -lz
|
LFLAGS += -lz
|
||||||
--- src/prop/cryptominisat.cpp.orig 2019-04-09 10:14:31.000000000 -0600
|
|
||||||
+++ src/prop/cryptominisat.cpp 2020-04-26 14:04:26.086833393 -0600
|
|
||||||
@@ -68,15 +68,8 @@ CryptoMinisatSolver::CryptoMinisatSolver
|
|
||||||
d_okay(true),
|
|
||||||
d_statistics(registry, name)
|
|
||||||
{
|
|
||||||
- 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;
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
@@ -154,10 +147,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;
|
|
||||||
}
|
|
||||||
|
|
||||||
--- src/prop/minisat/mtl/template.mk.orig 2019-04-09 10:14:31.000000000 -0600
|
--- src/prop/minisat/mtl/template.mk.orig 2019-04-09 10:14:31.000000000 -0600
|
||||||
+++ src/prop/minisat/mtl/template.mk 2019-04-17 11:22:15.879002442 -0600
|
+++ src/prop/minisat/mtl/template.mk 2019-04-17 11:22:15.879002442 -0600
|
||||||
@@ -22,7 +22,7 @@ CXX ?= g++
|
@@ -22,7 +22,7 @@ CXX ?= g++
|
||||||
|
|
Loading…
Reference in New Issue