From 55785ac04539943b5b7c3dffd2e3b4632cd87b2a Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Mon, 26 Mar 2012 11:45:42 +0000 Subject: [PATCH] Big speedup to utility code for producing the effect of the maximally precise propagator. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1613 e59a4935-1847-0410-ae03-e826735625c1 --- .../ConstantBitP_MaxPrecision.cpp | 114 ++++++++++-------- 1 file changed, 63 insertions(+), 51 deletions(-) diff --git a/src/simplifier/constantBitP/ConstantBitP_MaxPrecision.cpp b/src/simplifier/constantBitP/ConstantBitP_MaxPrecision.cpp index 30535f6..098bdfc 100644 --- a/src/simplifier/constantBitP/ConstantBitP_MaxPrecision.cpp +++ b/src/simplifier/constantBitP/ConstantBitP_MaxPrecision.cpp @@ -6,6 +6,7 @@ #include "../../to-sat/AIG/BBNodeManagerAIG.h" #include "../../absrefine_counterexample/AbsRefine_CounterExample.h" #include "../../to-sat/ASTNode/ToSAT.h" +#include "../../to-sat/AIG/ToSATAIG.h" #include "../../STPManager/STPManager.h" #include "../../sat/MinisatCore.h" @@ -98,6 +99,48 @@ void concretise(const ASTNode& variable, const FixedBits& fixed, ASTVec& list, S } +// Concretisation function. Gamma. +void concretise(const ASTNode& variable, const FixedBits& fixed, SATSolver::vec_literals& satSolverClause, STPMgr* beev, ToSATBase::ASTNodeToSATVar& map) +{ + if (BOOLEAN_TYPE == variable.GetType()) + { + assert(1 == fixed.getWidth()); + assert(fixed.isBoolean()); + + if (fixed.isFixed(0)) + { + if (!fixed.getValue(0)) // if it's false, try to find a true assignment. + { + assert(map.find(variable) != map.end()); + int v = (map.find(variable)->second)[0]; + satSolverClause.push(SATSolver::mkLit(v, false)); + } + else + { + assert(map.find(variable) != map.end()); + int v = (map.find(variable)->second)[0]; + satSolverClause.push(SATSolver::mkLit(v, true)); + } + + } + } + else + { + assert(BITVECTOR_TYPE == variable.GetType()); + assert(variable.GetValueWidth() == (unsigned)fixed.getWidth()); + for (int i = 0; i < fixed.getWidth(); i++) + { + if (fixed.isFixed(i)) + { + assert(map.find(variable) != map.end()); + int v = (map.find(variable)->second)[i]; + satSolverClause.push(SATSolver::mkLit(v, fixed.getValue(i))); + } + } + } +} + + // Concretisation function. Gamma. void concretiseB(const ASTNode& variable, const ASTNode& min, const ASTNode& max, ASTVec& list, STPMgr* beev) { @@ -323,20 +366,6 @@ bool maxBoundsPrecision(vector children, FixedBits& output, Kind kin return first; } - - - - - - - - - - - - - - // The bitWidth isn't necessarily the same for all children. e.g. ITE(boolean, x-bit, x-bit) bool maxPrecision(vector children, FixedBits& output, Kind kind, STPMgr* beev) { @@ -403,43 +432,36 @@ bool maxPrecision(vector children, FixedBits& output, Kind kind, STP expr = beev->CreateNode(BEEV::AND, expr, beev->CreateNode(BEEV::AND, notted)); } + bool first = true; - ASTVec ors; - ASTNode total = beev->ASTTrue; Simplifier simp(beev); ArrayTransformer at(beev,&simp); AbsRefine_CounterExample ce(beev,&simp,&at); - ToSAT tosat(beev); bool timeout = false; MinisatCore newS(timeout); + ToSATAIG tosat(beev); + tosat.setArrayTransformer(&at); + + SATSolver::vec_literals satSolverClause; + while (true) { - ASTNode toSolve; + + int result; if (first) { - toSolve = expr; + result = ce.CallSAT_ResultCheck(newS, expr, expr, &tosat,true); } else { - assert(ors.size() !=0); - if (ors.size() > 1) - toSolve = beev->CreateNode(BEEV::OR, ors); - else - toSolve = ors[0]; - ors.clear(); - } - - BVTypeCheck(toSolve); + assert(satSolverClause.size() > 0); + newS.addClause(satSolverClause); + satSolverClause.clear(); - // Some operations aren't bitblasted directly. For example sbvmod is converted into - // other operations first. - //ArrayTransformer(STPMgr * bm, Simplifier* s, NodeFactory &nodeFactory_) : - - toSolve = at.TransformFormula_TopLevel(toSolve); - total= beev->CreateNode(AND, total, toSolve); - int result = ce.CallSAT_ResultCheck(newS, total, total, &tosat,true); + result = ce.CallSAT_ResultCheck(newS, beev->ASTTrue, beev->ASTTrue, &tosat,true); + } if (2 == result) FatalError("error from solver"); @@ -456,13 +478,13 @@ bool maxPrecision(vector children, FixedBits& output, Kind kind, STP { ASTNode n = (ce.GetCounterExample(true, variables[i])); *children[i] = FixedBits::concreteToAbstract(n); - concretise(variables[i], *(children[i]), ors, beev); + concretise(variables[i], *(children[i]), satSolverClause, beev, tosat.SATVar_to_SymbolIndexMap()); } ASTNode n = (ce.GetCounterExample(true, outputNode)); output = FixedBits::concreteToAbstract(n); //cerr << resultNode.GetName() << " " << n << endl; - concretise(outputNode, output, ors, beev); + concretise(outputNode, output, satSolverClause, beev, tosat.SATVar_to_SymbolIndexMap()); } else { @@ -471,32 +493,22 @@ bool maxPrecision(vector children, FixedBits& output, Kind kind, STP ASTNode n = (ce.GetCounterExample(true, variables[i])); //cerr << variables[i].GetName() << " " << n << endl; *children[i] = FixedBits::meet(FixedBits::concreteToAbstract(n), *children[i]); - concretise(variables[i], *(children[i]), ors, beev); + concretise(variables[i], *(children[i]), satSolverClause, beev, tosat.SATVar_to_SymbolIndexMap()); } ASTNode n = (ce.GetCounterExample(true, outputNode)); output = FixedBits::meet(FixedBits::concreteToAbstract(n), output); //cerr << resultNode.GetName() << " " << n << endl; - concretise(outputNode, output, ors, beev); + concretise(outputNode, output, satSolverClause, beev,tosat.SATVar_to_SymbolIndexMap()); } first = false; - //print(children, output, kind); - - if (0 == ors.size()) - break; // everything is at top. - - //beev->AddAssert(beev->CreateNode(BEEV::OR, ors)); + if (satSolverClause.size() == 0) + break; // everything is at top. } - //beev->ClearSATTables(); - //beev->ClearAllCaches(); - - // The first time we AddAsserts() it creates a new ASTVec to store them (on the heap). - //beev->Pop(); - beev->UserFlags.bitConstantProp_flag = !disabledProp; beev->UserFlags.print_output_flag = printOutput; -- 2.47.3