From aef1e3e66ecfd1d1e57ae52c951d5d62d54f69e7 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Mon, 5 Apr 2010 12:22:14 +0000 Subject: [PATCH] Enable the simplifying node factory when parsing smt-lib format file. BVConstEvaluator now does the logical operations too. I moved them over from CounterExample. I realise they no longer short-cut nicely, but don't believe it matters. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@664 e59a4935-1847-0410-ae03-e826735625c1 --- .../CounterExample.cpp | 152 ++++++---------- src/main/main.cpp | 5 +- src/simplifier/consteval.cpp | 169 +++++++++++++++--- src/simplifier/simplifier.h | 2 - 4 files changed, 205 insertions(+), 123 deletions(-) diff --git a/src/absrefine_counterexample/CounterExample.cpp b/src/absrefine_counterexample/CounterExample.cpp index 35796be..4241a42 100644 --- a/src/absrefine_counterexample/CounterExample.cpp +++ b/src/absrefine_counterexample/CounterExample.cpp @@ -404,9 +404,10 @@ namespace BEEV } default: { - ASTVec c = term.GetChildren(); + const ASTVec& c = term.GetChildren(); ASTVec o; - for (ASTVec::iterator + o.reserve(c.size()); + for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it != itend; it++) { ASTNode ff = TermToConstTermUsingModel(*it, ArrayReadFlag); @@ -508,8 +509,8 @@ namespace BEEV ASTNode AbsRefine_CounterExample::ComputeFormulaUsingModel(const ASTNode& form) { - ASTNode in = form; - Kind k = form.GetKind(); + const ASTNode& in = form; + const Kind k = form.GetKind(); if (!(is_Form_kind(k) && BOOLEAN_TYPE == form.GetType())) { FatalError(" ComputeConstFormUsingModel: "\ @@ -532,8 +533,7 @@ namespace BEEV } } - ASTNode t0, t1; - ASTNode output = ASTFalse; + ASTNode output = ASTUndefined; switch (k) { case TRUE: @@ -570,106 +570,60 @@ namespace BEEV case BVSLT: case BVSLE: case BVSGT: - case BVSGE: - //convert form[0] into a constant term - t0 = TermToConstTermUsingModel(form[0], false); - //convert form[0] into a constant term - t1 = TermToConstTermUsingModel(form[1], false); - output = simp->BVConstEvaluator(bm->CreateNode(k, t0, t1)); - - //evaluate formula to false if bvdiv execption occurs while - //counterexample is being checked during refinement. - if (bm->bvdiv_exception_occured - && bm->counterexample_checking_during_refinement) - { - output = ASTFalse; - } - break; + case BVSGE: { + ASTVec children; + children.reserve(form.Degree()); + + for (ASTVec::const_iterator it = form.begin(), itend = form.end(); it + != itend; it++) { + children.push_back(TermToConstTermUsingModel(*it, false)); + } + + output = simp->BVConstEvaluator(bm->CreateNode(k, children)); + + //evaluate formula to false if bvdiv execption occurs while + //counterexample is being checked during refinement. + if (bm->bvdiv_exception_occured + && bm->counterexample_checking_during_refinement) { + output = ASTFalse; + } + + } + break; + case NAND: - { - ASTNode o = ASTTrue; - for (ASTVec::const_iterator - it = form.begin(), itend = form.end(); it != itend; it++) - if (ASTFalse == ComputeFormulaUsingModel(*it)) - { - o = ASTFalse; - break; - } - if (o == ASTTrue) - output = ASTFalse; - else - output = ASTTrue; - break; - } case NOR: - { - ASTNode o = ASTFalse; - for (ASTVec::const_iterator - it = form.begin(), itend = form.end(); it != itend; it++) - if (ASTTrue == ComputeFormulaUsingModel(*it)) - { - o = ASTTrue; - break; - } - if (o == ASTTrue) - output = ASTFalse; - else - output = ASTTrue; - break; - } case NOT: - if (ASTTrue == ComputeFormulaUsingModel(form[0])) - output = ASTFalse; - else - output = ASTTrue; - break; - case OR: - for (ASTVec::const_iterator - it = form.begin(), itend = form.end(); it != itend; it++) - if (ASTTrue == ComputeFormulaUsingModel(*it)) - output = ASTTrue; - break; case AND: - output = ASTTrue; - for (ASTVec::const_iterator - it = form.begin(), itend = form.end(); it != itend; it++) - { - if (ASTFalse == ComputeFormulaUsingModel(*it)) - { - output = ASTFalse; - break; - } - } - break; case XOR: - t0 = ComputeFormulaUsingModel(form[0]); - t1 = ComputeFormulaUsingModel(form[1]); - if ((ASTTrue == t0 - && ASTTrue == t1) - || (ASTFalse == t0 && ASTFalse == t1)) - output = ASTFalse; - else - output = ASTTrue; - break; case IFF: - t0 = ComputeFormulaUsingModel(form[0]); - t1 = ComputeFormulaUsingModel(form[1]); - if ((ASTTrue == t0 && ASTTrue == t1) - || (ASTFalse == t0 && ASTFalse == t1)) - output = ASTTrue; - else - output = ASTFalse; - break; case IMPLIES: - t0 = ComputeFormulaUsingModel(form[0]); - t1 = ComputeFormulaUsingModel(form[1]); - if ((ASTFalse == t0) || (ASTTrue == t0 && ASTTrue == t1)) - output = ASTTrue; - else - output = ASTFalse; + case OR: + { + ASTVec children; + children.reserve(form.Degree()); + + for (ASTVec::const_iterator it = form.begin(), itend = form.end(); it != itend; it++) + { + children.push_back( ComputeFormulaUsingModel(*it)); + } + + output = simp->BVConstEvaluator(bm->CreateNode(k, children)); + + //evaluate formula to false if bvdiv execption occurs while + //counterexample is being checked during refinement. + if (bm->bvdiv_exception_occured + && bm->counterexample_checking_during_refinement) + { + output = ASTFalse; + } + + } break; + case ITE: - t0 = ComputeFormulaUsingModel(form[0]); + { + ASTNode t0 = ComputeFormulaUsingModel(form[0]); if (ASTTrue == t0) output = ComputeFormulaUsingModel(form[1]); else if (ASTFalse == t0) @@ -677,6 +631,7 @@ namespace BEEV else FatalError("ComputeFormulaUsingModel: ITE: "\ "something is wrong with the formula: ", form); + } break; case PARAMBOOL: output = bm->NewParameterized_BooleanVar(form[0],form[1]); @@ -687,12 +642,15 @@ namespace BEEV output = ASTTrue; break; default: + cerr << _kind_names[k]; FatalError(" ComputeFormulaUsingModel: "\ "the kind has not been implemented", ASTUndefined); break; } //cout << "ComputeFormulaUsingModel output is:" << output << endl; + assert(ASTUndefined != output); + assert(output.isConstant()); ComputeFormulaMap[form] = output; return output; } diff --git a/src/main/main.cpp b/src/main/main.cpp index b7f5f84..bc70f3c 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -336,10 +336,11 @@ int main(int argc, char ** argv) { { // Wrap a typchecking node factory around the default node factory. // every node created is typechecked. - TypeChecker nf(*bm->defaultNodeFactory,*bm); + SimplifyingNodeFactory simpNF(*bm->defaultNodeFactory,*bm); + TypeChecker nf(simpNF,*bm); // Changes need to be made to the constant evaluator to get this working. - //SimplifyingNodeFactory nf3(nf,*bm); + ParserInterface pi(*bm, &nf); parserInterface = π diff --git a/src/simplifier/consteval.cpp b/src/simplifier/consteval.cpp index d809785..58d2c2f 100644 --- a/src/simplifier/consteval.cpp +++ b/src/simplifier/consteval.cpp @@ -1,6 +1,6 @@ // -*- c++ -*- /******************************************************************** - * AUTHORS: Vijay Ganesh + * AUTHORS: Vijay Ganesh, Trevor Hansen * * BEGIN DATE: November, 2005 * @@ -21,6 +21,7 @@ namespace BEEV FatalError(ss.c_str(), t); } +// Const evaluator logical and arithmetic operations. ASTNode Simplifier::BVConstEvaluator(const ASTNode& t) { ASTNode OutputNode; @@ -37,18 +38,31 @@ namespace BEEV CBV tmp0 = NULL; CBV tmp1 = NULL; + ASTVec children; + children.reserve(t.Degree()); + for (int i =0; i < t.Degree(); i++) + { + if (t[i].isConstant()) + children.push_back(t[i]); + else + children.push_back(BVConstEvaluator(t[i])); + } + + if ((t.Degree() ==2 || t.Degree() == 1) && t[0].GetType() == BITVECTOR_TYPE) + { //saving some typing. BVPLUS does not use these variables. if the //input BVPLUS has two nodes, then we want to avoid setting these //variables. if (1 == t.Degree()) { - tmp0 = BVConstEvaluator(t[0]).GetBVConst(); + tmp0 = children[0].GetBVConst(); } else if (2 == t.Degree() && k != BVPLUS) { - tmp0 = BVConstEvaluator(t[0]).GetBVConst(); - tmp1 = BVConstEvaluator(t[1]).GetBVConst(); + tmp0 = children[0].GetBVConst(); + tmp1 = children[1].GetBVConst(); } + } switch (k) { @@ -56,10 +70,9 @@ namespace BEEV case READ: case WRITE: case SYMBOL: - FatalError("BVConstEvaluator: term is not a constant-term", t); + FatalError("BVConstEvaluator: term is not a constant-term", t); break; case BVCONST: - //FIXME Handle this special case better OutputNode = t; break; case BVNEG: @@ -72,7 +85,6 @@ namespace BEEV case BVSX: { output = CONSTANTBV::BitVector_Create(inputwidth, true); - //unsigned * out0 = BVConstEvaluator(t[0]).GetBVConst(); unsigned t0_width = t[0].GetValueWidth(); if (inputwidth == t0_width) { @@ -106,7 +118,7 @@ namespace BEEV output = CONSTANTBV::BitVector_Create(inputwidth, true); // Number of bits to shift it. - ASTNode shiftNode = BVConstEvaluator(t[1]); + ASTNode shiftNode = children[1]; bool msb = CONSTANTBV::BitVector_msb_(tmp0); @@ -186,9 +198,9 @@ namespace BEEV case BVEXTRACT: { output = CONSTANTBV::BitVector_Create(inputwidth, true); - tmp0 = BVConstEvaluator(t[0]).GetBVConst(); - unsigned int hi = GetUnsignedConst(BVConstEvaluator(t[1])); - unsigned int low = GetUnsignedConst(BVConstEvaluator(t[2])); + tmp0 = children[0].GetBVConst(); + unsigned int hi = GetUnsignedConst(children[1]); + unsigned int low = GetUnsignedConst(children[2]); unsigned int len = hi - low + 1; CONSTANTBV::BitVector_Destroy(output); @@ -203,8 +215,8 @@ namespace BEEV { assert(2==t.Degree()); output = CONSTANTBV::BitVector_Create(inputwidth, true); - unsigned t0_width = t[0].GetValueWidth(); - unsigned t1_width = t[1].GetValueWidth(); + unsigned t0_width = children[0].GetValueWidth(); + unsigned t1_width = children[1].GetValueWidth(); CONSTANTBV::BitVector_Destroy(output); output = CONSTANTBV::BitVector_Concat(tmp0, tmp1); @@ -234,10 +246,9 @@ namespace BEEV { output = CONSTANTBV::BitVector_Create(inputwidth, true); bool carry = false; - ASTVec c = t.GetChildren(); - for (ASTVec::iterator it = c.begin(), itend = c.end(); it != itend; it++) + for (ASTVec::iterator it = children.begin(), itend = children.end(); it != itend; it++) { - CBV kk = BVConstEvaluator(*it).GetBVConst(); + CBV kk = (*it).GetBVConst(); CONSTANTBV::BitVector_add(output, output, kk, &carry); carry = false; //CONSTANTBV::BitVector_Destroy(kk); @@ -468,12 +479,10 @@ namespace BEEV } case ITE: { - ASTNode tmp0 = t[0]; // Should this run BVConstEvaluator?? - - if (ASTTrue == tmp0) - OutputNode = BVConstEvaluator(t[1]); - else if (ASTFalse == tmp0) - OutputNode = BVConstEvaluator(t[2]); + if (ASTTrue == t[0]) + OutputNode = children[1]; + else if (ASTFalse == t[0]) + OutputNode = children[2]; else { cerr << tmp0; @@ -547,6 +556,121 @@ namespace BEEV OutputNode = ASTFalse; break; } + + case TRUE: + OutputNode = ASTTrue; + break; + case FALSE: + OutputNode = ASTFalse; + break; + case NOT: + if (ASTTrue == t[0]) + return ASTFalse; + else if (ASTFalse == t[0]) + return ASTTrue; + else + { + cerr << ASTFalse; + cerr << t[0]; + FatalError("BVConstEvaluator: unexpected not input", t); + } + + case OR: + OutputNode = ASTFalse; + for (ASTVec::const_iterator it = children.begin(), itend = children.end(); it != itend; it++) + if (ASTTrue == *it) + OutputNode = ASTTrue; + + + break; + + case NOR: + { + ASTNode o = ASTFalse; + for (ASTVec::const_iterator it = children.begin(), itend = + children.end(); it != itend; it++) + if (ASTTrue == (*it)) { + o = ASTTrue; + break; + } + if (o == ASTTrue) + OutputNode = ASTFalse; + else + OutputNode = ASTTrue; + break; + } + + + case XOR: + { + bool output = false; + for (ASTVec::const_iterator it = children.begin(), itend = + children.end(); it != itend; it++) + { + if (ASTTrue == *it) + output = !output; //parity. + } + + if (output) + OutputNode = ASTTrue; + else + OutputNode = ASTFalse; + + break; + + + } + + case AND: + { + OutputNode = ASTTrue; + for (ASTVec::const_iterator it = children.begin(), itend = children.end(); it != itend; it++) + { + if (ASTFalse == (*it)) + { + OutputNode = ASTFalse; + break; + } + } + break; + } + + case NAND: + { OutputNode = ASTFalse; + for (ASTVec::const_iterator it = children.begin(), itend = children.end(); it != itend; it++) + { + if (ASTFalse == (*it)) + { + OutputNode = ASTTrue; + break; + } + } + break; + } + + + case IFF: + { + const ASTNode& t0 = children[0]; + const ASTNode& t1 = children[1]; + if ((ASTTrue == t0 && ASTTrue == t1) || (ASTFalse == t0 && ASTFalse == t1)) + OutputNode = ASTTrue; + else + OutputNode = ASTFalse; + break; + } + + case IMPLIES: + { + const ASTNode& t0 = children[0]; + const ASTNode& t1 = children[1]; + if ((ASTFalse == t0) || (ASTTrue == t0 && ASTTrue == t1)) + OutputNode = ASTTrue; + else + OutputNode = ASTFalse; + break; + } + default: FatalError("BVConstEvaluator: The input kind is not supported yet:", t); break; @@ -561,6 +685,7 @@ namespace BEEV cerr<