From bb6c74a7bb306de8b7c5d7e9701b3524eda68f4a Mon Sep 17 00:00:00 2001 From: Dejan Jovanović Date: Wed, 3 Apr 2013 17:55:58 -0400 Subject: * changing the bitblast-eager to bitblast on pre-register * the newVar interface of the sat solver now changed to include (isTheoryLiteral, preRegister, canEliminate) * when bitblast-eager all bv atoms are (theory=false, prereg = true, canelim = true) * bitblast-eager implies decision=internal --- src/prop/minisat/minisat.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/prop/minisat/minisat.cpp') diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index 886dc0f72..960f2ad62 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -140,8 +140,8 @@ void MinisatSatSolver::addClause(SatClause& clause, bool removable) { d_minisat->addClause(minisat_clause, removable); } -SatVariable MinisatSatSolver::newVar(bool theoryAtom) { - return d_minisat->newVar(true, true, theoryAtom); +SatVariable MinisatSatSolver::newVar(bool isTheoryAtom, bool preRegister, bool canErase) { + return d_minisat->newVar(true, true, isTheoryAtom, preRegister, canErase); } SatValue MinisatSatSolver::solve(unsigned long& resource) { -- cgit v1.2.3