diff options
author | lianah <lianahady@gmail.com> | 2013-04-18 19:09:44 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-04-18 19:09:44 -0400 |
commit | c863478fd87b4ff7d97d00a4a63a4c5e9bac2b4b (patch) | |
tree | a4417d4a56733f660a8e410db35addda1f0cacfe | |
parent | eaa9f9af40941ef1aeb93367884e692301b60280 (diff) | |
parent | 8d56bb7184d573448fd16242afda2e4224e8641d (diff) |
Merge branch 'master' of https://github.com/CVC4/CVC4
-rw-r--r-- | src/parser/tptp/Tptp.g | 2 | ||||
-rw-r--r-- | src/parser/tptp/tptp.h | 33 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 14 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 5 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 1 | ||||
-rw-r--r-- | src/theory/booleans/theory_bool_rewriter.cpp | 127 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_bitblast.cpp | 48 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_bitblast.h | 8 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_core.cpp | 19 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_inequality.cpp | 11 | ||||
-rw-r--r-- | test/regress/regress0/preprocess/Makefile.am | 5 | ||||
-rw-r--r-- | test/regress/regress0/preprocess/preprocess_13.cvc | 10 | ||||
-rw-r--r-- | test/regress/regress0/preprocess/preprocess_14.cvc | 12 | ||||
-rw-r--r-- | test/regress/regress0/preprocess/preprocess_15.cvc | 12 | ||||
-rw-r--r-- | test/unit/prop/cnf_stream_white.h | 2 |
15 files changed, 217 insertions, 92 deletions
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index 80736caa5..9e814b358 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -290,7 +290,7 @@ simpleTerm[CVC4::Expr& expr] : variable[expr] | NUMBER { expr = PARSER_STATE->d_tmp_expr; } | DISTINCT_OBJECT { expr = PARSER_STATE->convertStrToUnsorted( - MK_CONST(AntlrInput::tokenText($DISTINCT_OBJECT))); } + AntlrInput::tokenText($DISTINCT_OBJECT)); } ; functionTerm[CVC4::Expr& expr] diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h index adaca892f..6b7adbbf7 100644 --- a/src/parser/tptp/tptp.h +++ b/src/parser/tptp/tptp.h @@ -21,6 +21,7 @@ #include "parser/parser.h" #include "expr/command.h" +#include "util/hash.h" #include <ext/hash_set> #include <cassert> @@ -42,7 +43,7 @@ class Tptp : public Parser { Expr d_uts_op; // The set of expression that already have a bridge std::hash_set<Expr, ExprHashFunction> d_r_converted; - std::hash_set<Expr, ExprHashFunction> d_s_converted; + std::hash_map<std::string, Expr, StringHashFunction> d_distinct_objects; //TPTP directory where to find includes // empty if none could be determined @@ -87,32 +88,12 @@ public: return ret; } - inline Expr convertStrToUnsorted(Expr expr){ - ExprManager * em = getExprManager(); - - // Create the conversion function If they doesn't exists - if(d_stu_op.isNull()){ - Type t; - //Conversion from string to unsorted - t = em->mkFunctionType(em->stringType(), d_unsorted); - d_stu_op = em->mkVar("$$stu",t); - preemptCommand(new DeclareFunctionCommand("$$stu", d_stu_op, t)); - //Conversion from unsorted to string - t = em->mkFunctionType(d_unsorted, em->stringType()); - d_uts_op = em->mkVar("$$uts",t); - preemptCommand(new DeclareFunctionCommand("$$uts", d_uts_op, t)); + inline Expr convertStrToUnsorted(std::string str) { + Expr& e = d_distinct_objects[str]; + if(e.isNull()) { + e = getExprManager()->mkConst(UninterpretedConstant(d_unsorted, d_distinct_objects.size() - 1)); } - // Add the inverse in order to show that over the elements that - // appear in the problem there is a bijection between unsorted and - // rational - Expr ret = em->mkExpr(kind::APPLY_UF,d_stu_op,expr); - if ( d_s_converted.find(expr) == d_s_converted.end() ){ - d_s_converted.insert(expr); - Expr eq = em->mkExpr(kind::EQUAL,expr, - em->mkExpr(kind::APPLY_UF,d_uts_op,ret)); - preemptCommand(new AssertCommand(eq)); - }; - return ret; + return e; } public: diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 35db0975e..0d9d63d91 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -749,8 +749,8 @@ SmtEngine::~SmtEngine() throw() { // global push/pop around everything, to ensure proper destruction // of context-dependent data structures - d_context->pop(); - d_userContext->pop(); + d_context->popto(0); + d_userContext->popto(0); if(d_assignments != NULL) { d_assignments->deleteSelf(); @@ -771,18 +771,18 @@ SmtEngine::~SmtEngine() throw() { d_definedFunctions->deleteSelf(); - delete d_stats; - - delete d_private; delete d_theoryEngine; delete d_propEngine; delete d_decisionEngine; - delete d_userContext; - + delete d_stats; delete d_statisticsRegistry; + delete d_private; + + delete d_userContext; + } catch(Exception& e) { Warning() << "CVC4 threw an exception during cleanup." << endl << e << endl; diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 53cdd3fdc..801893107 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -87,6 +87,7 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC d_decisionRequests(c), d_permRef(c), d_modelConstraints(c), + d_lemmasSaved(c), d_inCheckModel(false) { StatisticsRegistry::registerStat(&d_numRow); @@ -1294,6 +1295,10 @@ void TheoryArrays::checkModel(Effort e) while (!d_lemmas.empty()) { Debug("arrays-model-based") << "Sending lemma: " << d_lemmas.back() << endl; d_out->lemma(d_lemmas.back()); +#ifdef CVC4_ASSERTIONS + Assert(d_lemmasSaved.find(d_lemmas.back()) == d_lemmasSaved.end()); + d_lemmasSaved.insert(d_lemmas.back()); +#endif d_lemmas.pop_back(); } Assert(getSatContext()->getLevel() == d_topLevel); diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 39fd90012..e0191ccc9 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -358,6 +358,7 @@ class TheoryArrays : public Theory { // List of nodes that need permanent references in this context context::CDList<Node> d_permRef; context::CDList<Node> d_modelConstraints; + context::CDHashSet<Node, NodeHashFunction > d_lemmasSaved; std::vector<Node> d_lemmas; Node getSkolem(TNode ref, const std::string& name, const TypeNode& type, const std::string& comment, bool makeEqual = true); diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp index d6aa51aba..9867ccd4e 100644 --- a/src/theory/booleans/theory_bool_rewriter.cpp +++ b/src/theory/booleans/theory_bool_rewriter.cpp @@ -22,6 +22,72 @@ namespace CVC4 { namespace theory { namespace booleans { +/** + * flattenNode looks for children of same kind, and if found merges + * them into the parent. + * + * It simultaneously handles a couple of other optimizations: + * - trivialNode - if found during exploration, return that node itself + * (like in case of OR, if "true" is found, makes sense to replace + * whole formula with "true") + * - skipNode - as name suggests, skip them + * (like in case of OR, you may want to skip any "false" nodes found) + * + * Use a null node if you want to ignore any of the optimizations. + */ +RewriteResponse flattenNode(TNode n, TNode trivialNode, TNode skipNode) +{ + typedef std::hash_set<TNode, TNodeHashFunction> node_set; + + node_set visited; + visited.insert(skipNode); + + std::vector<TNode> toProcess; + toProcess.push_back(n); + + Kind k = n.getKind(); + typedef std::vector<TNode> ChildList; + ChildList childList; //TNode should be fine, since 'n' is still there + + for (unsigned i = 0; i < toProcess.size(); ++ i) { + TNode current = toProcess[i]; + for(unsigned j = 0, j_end = current.getNumChildren(); j < j_end; ++ j) { + TNode child = current[j]; + if(visited.find(child) != visited.end()) { + continue; + } else if(child == trivialNode) { + return RewriteResponse(REWRITE_DONE, trivialNode); + } else { + visited.insert(child); + if(child.getKind() == k) + toProcess.push_back(child); + else + childList.push_back(child); + } + } + } + if (childList.size() == 0) return RewriteResponse(REWRITE_DONE, skipNode); + if (childList.size() == 1) return RewriteResponse(REWRITE_AGAIN, childList[0]); + + /* Trickery to stay under number of children possible in a node */ + NodeManager* nodeManager = NodeManager::currentNM(); + static const unsigned MAX_CHILDREN = (1u << __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN ) - 1; + if (childList.size() < MAX_CHILDREN) { + Node retNode = nodeManager->mkNode(k, childList); + return RewriteResponse(REWRITE_DONE, retNode); + } else { + Assert(childList.size() < size_t(MAX_CHILDREN) * size_t(MAX_CHILDREN) ); + NodeBuilder<> nb(k); + ChildList::iterator cur = childList.begin(), next, en = childList.end(); + while( cur != en ) { + next = min(cur + MAX_CHILDREN, en); + nb << (nodeManager->mkNode(k, ChildList(cur, next) )); + cur = next; + } + return RewriteResponse(REWRITE_DONE, nb.constructNode()); + } +} + RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { NodeManager* nodeManager = NodeManager::currentNM(); Node tt = nodeManager->mkConst(true); @@ -35,55 +101,30 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { break; } case kind::OR: { - if (n.getNumChildren() == 2) { - if (n[0] == tt || n[1] == tt) return RewriteResponse(REWRITE_DONE, tt); - if (n[0] == ff) return RewriteResponse(REWRITE_AGAIN, n[1]); - if (n[1] == ff) return RewriteResponse(REWRITE_AGAIN, n[0]); + bool done = true; + TNode::iterator i = n.begin(), iend = n.end(); + for(; i != iend; ++i) { + if (*i == tt) return RewriteResponse(REWRITE_DONE, tt); + if (*i == ff) done = false; + if ((*i).getKind() == kind::OR) done = false; } - else { - bool done = true; - TNode::iterator i = n.begin(), iend = n.end(); - for(; i != iend; ++i) { - if (*i == tt) return RewriteResponse(REWRITE_DONE, tt); - if (*i == ff) done = false; - } - if (!done) { - NodeBuilder<> nb(kind::OR); - for(i = n.begin(); i != iend; ++i) { - if (*i != ff) nb << *i; - } - if (nb.getNumChildren() == 0) return RewriteResponse(REWRITE_DONE, ff); - if (nb.getNumChildren() == 1) return RewriteResponse(REWRITE_AGAIN, nb.getChild(0)); - return RewriteResponse(REWRITE_AGAIN, nb.constructNode()); - } + if (!done) { + return flattenNode(n, /*trivialNode = */ tt, /* skipNode = */ ff); } break; } case kind::AND: { - //TODO: Why REWRITE_AGAIN here? - if (n.getNumChildren() == 2) { - if (n[0] == ff || n[1] == ff) return RewriteResponse(REWRITE_DONE, ff); - if (n[0] == tt) return RewriteResponse(REWRITE_AGAIN, n[1]); - if (n[1] == tt) return RewriteResponse(REWRITE_AGAIN, n[0]); + bool done = true; + TNode::iterator i = n.begin(), iend = n.end(); + for(; i != iend; ++i) { + if (*i == ff) return RewriteResponse(REWRITE_DONE, ff); + if (*i == tt) done = false; + if ((*i).getKind() == kind::AND) done = false; } - else { - bool done = true; - TNode::iterator i = n.begin(), iend = n.end(); - for(; i != iend; ++i) { - if (*i == ff) return RewriteResponse(REWRITE_DONE, ff); - if (*i == tt) done = false; - } - if (!done) { - NodeBuilder<> nb(kind::AND); - for(i = n.begin(); i != iend; ++i) { - if (*i != tt) { - nb << *i; - } - } - if (nb.getNumChildren() == 0) return RewriteResponse(REWRITE_DONE, tt); - if (nb.getNumChildren() == 1) return RewriteResponse(REWRITE_AGAIN, nb.getChild(0)); - return RewriteResponse(REWRITE_AGAIN, nb.constructNode()); - } + if (!done) { + RewriteResponse ret = flattenNode(n, /*trivialNode = */ ff, /* skipNode = */ tt); + Debug("bool-flatten") << n << ": " << ret.node << std::endl; + return ret; } break; } diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp index d8a784544..997244c40 100644 --- a/src/theory/bv/bv_subtheory_bitblast.cpp +++ b/src/theory/bv/bv_subtheory_bitblast.cpp @@ -31,7 +31,8 @@ BitblastSolver::BitblastSolver(context::Context* c, TheoryBV* bv) : SubtheorySolver(c, bv), d_bitblaster(new Bitblaster(c, bv)), d_bitblastQueue(c), - d_statistics() + d_statistics(), + d_validModelCache(c, true) {} BitblastSolver::~BitblastSolver() { @@ -87,6 +88,7 @@ bool BitblastSolver::check(Theory::Effort e) { // Processing assertions while (!done()) { TNode fact = get(); + d_validModelCache = false; Debug("bv-bitblast") << " fact " << fact << ")\n"; if (!d_bv->inConflict() && (!d_bv->wasPropagatedBySubtheory(fact) || d_bv->getPropagatingSubtheory(fact) != SUB_BITBLAST)) { // Some atoms have not been bit-blasted yet @@ -138,8 +140,46 @@ void BitblastSolver::collectModelInfo(TheoryModel* m) { return d_bitblaster->collectModelInfo(m); } -Node BitblastSolver::getModelValue(TNode node) { - Node val = d_bitblaster->getVarValue(node); - Assert (val != Node() || d_bv->isSharedTerm(node)); +Node BitblastSolver::getModelValue(TNode node) +{ + if (!d_validModelCache) { + d_modelCache.clear(); + d_validModelCache = true; + } + return getModelValueRec(node); +} + +Node BitblastSolver::getModelValueRec(TNode node) +{ + Node val; + if (node.isConst()) { + return node; + } + NodeMap::iterator it = d_modelCache.find(node); + if (it != d_modelCache.end()) { + val = (*it).second; + Debug("bitvector-model") << node << " => (cached) " << val <<"\n"; + return val; + } + if (d_bv->isLeaf(node)) { + val = d_bitblaster->getVarValue(node); + if (val == Node()) { + // If no value in model, just set to 0 + val = utils::mkConst(utils::getSize(node), (unsigned)0); + } + } else { + NodeBuilder<> valBuilder(node.getKind()); + if (node.getMetaKind() == kind::metakind::PARAMETERIZED) { + valBuilder << node.getOperator(); + } + for (unsigned i = 0; i < node.getNumChildren(); ++i) { + valBuilder << getModelValueRec(node[i]); + } + val = valBuilder; + val = Rewriter::rewrite(val); + } + Assert(val.isConst()); + d_modelCache[node] = val; + Debug("bitvector-model") << node << " => " << val <<"\n"; return val; } diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h index 1fab621cd..819b3d62c 100644 --- a/src/theory/bv/bv_subtheory_bitblast.h +++ b/src/theory/bv/bv_subtheory_bitblast.h @@ -19,7 +19,7 @@ #pragma once #include "theory/bv/bv_subtheory.h" - +#include "theory/substitutions.h" namespace CVC4 { namespace theory { namespace bv { @@ -41,6 +41,12 @@ class BitblastSolver : public SubtheorySolver { /** Nodes that still need to be bit-blasted */ context::CDQueue<TNode> d_bitblastQueue; Statistics d_statistics; + + typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap; + NodeMap d_modelCache; + context::CDO<bool> d_validModelCache; + Node getModelValueRec(TNode node); + public: BitblastSolver(context::Context* c, TheoryBV* bv); ~BitblastSolver(); diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp index a1c8f0e9a..c0546f892 100644 --- a/src/theory/bv/bv_subtheory_core.cpp +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -387,17 +387,26 @@ void CoreSolver::collectModelInfo(TheoryModel* m) { } Node CoreSolver::getModelValue(TNode var) { + // we don't need to evaluate bv expressions and only look at variable values + // because this only gets called when the core theory is complete (i.e. no other bv + // function symbols are currently asserted) + Assert (d_slicer->isCoreTerm(var)); + + Debug("bitvector-model") << "CoreSolver::getModelValue (" << var <<")"; Assert (isComplete()); TNode repr = d_equalityEngine.getRepresentative(var); + Node result = Node(); if (repr.getKind() == kind::CONST_BITVECTOR) { - return repr; - } - if (d_modelValues.find(repr) == d_modelValues.end()) { + result = repr; + } else if (d_modelValues.find(repr) == d_modelValues.end()) { // it may be a shared term that never gets asserted + // result is just Null Assert(d_bv->isSharedTerm(var)); - return Node(); + } else { + result = d_modelValues[repr]; } - return d_modelValues[repr]; + Debug("bitvector-model") << " => " << result <<"\n"; + return result; } CoreSolver::Statistics::Statistics() diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp index 40093f070..f45250f5b 100644 --- a/src/theory/bv/bv_subtheory_inequality.cpp +++ b/src/theory/bv/bv_subtheory_inequality.cpp @@ -178,13 +178,18 @@ void InequalitySolver::collectModelInfo(TheoryModel* m) { } Node InequalitySolver::getModelValue(TNode var) { + Assert (isInequalityOnly(var)); + Debug("bitvector-model") << "InequalitySolver::getModelValue (" << var <<")"; Assert (isComplete()); + Node result = Node(); if (!d_inequalityGraph.hasValueInModel(var)) { Assert (d_bv->isSharedTerm(var)); - return Node(); + } else { + BitVector val = d_inequalityGraph.getValueInModel(var); + result = utils::mkConst(val); } - BitVector val = d_inequalityGraph.getValueInModel(var); - return utils::mkConst(val); + Debug("bitvector-model") << " => " << result <<"\n"; + return result; } InequalitySolver::Statistics::Statistics() diff --git a/test/regress/regress0/preprocess/Makefile.am b/test/regress/regress0/preprocess/Makefile.am index 96b5d2928..fe02b230e 100644 --- a/test/regress/regress0/preprocess/Makefile.am +++ b/test/regress/regress0/preprocess/Makefile.am @@ -37,7 +37,10 @@ CVC_TESTS = \ preprocess_09.cvc \ preprocess_10.cvc \ preprocess_11.cvc \ - preprocess_12.cvc + preprocess_12.cvc \ + preprocess_13.cvc \ + preprocess_14.cvc \ + preprocess_15.cvc # Regression tests derived from bug reports BUG_TESTS = diff --git a/test/regress/regress0/preprocess/preprocess_13.cvc b/test/regress/regress0/preprocess/preprocess_13.cvc new file mode 100644 index 000000000..7a2ed7dd8 --- /dev/null +++ b/test/regress/regress0/preprocess/preprocess_13.cvc @@ -0,0 +1,10 @@ +% EXPECT: valid + +a0, a1, a2, a3, a4, a5, a6, a7, a8, a9: BOOLEAN; + +ASSERT (a5); + +QUERY (a0 OR (a1 OR (a2 OR (a3 OR (a4 OR (a5 OR (FALSE OR (a6 OR (a7 OR (a8 OR a9)))))))))); + +% EXIT: 20 + diff --git a/test/regress/regress0/preprocess/preprocess_14.cvc b/test/regress/regress0/preprocess/preprocess_14.cvc new file mode 100644 index 000000000..04a6f4c50 --- /dev/null +++ b/test/regress/regress0/preprocess/preprocess_14.cvc @@ -0,0 +1,12 @@ +% EXPECT: sat + +a0, a1, a2, a3, a4, a5, a6, a7, a8, a9: BOOLEAN; + +ASSERT (a5); + +ASSERT (a0 OR (a1 AND (a2 OR (a3 AND (a4 AND (a5 AND (TRUE AND (a6 AND (a7 AND (a8 AND a9)))))))))); + +CHECKSAT; + +% EXIT: 10 + diff --git a/test/regress/regress0/preprocess/preprocess_15.cvc b/test/regress/regress0/preprocess/preprocess_15.cvc new file mode 100644 index 000000000..30df35e53 --- /dev/null +++ b/test/regress/regress0/preprocess/preprocess_15.cvc @@ -0,0 +1,12 @@ +% EXPECT: sat + +a0, a1, a2, a3, a4, a5, a6, a7, a8, a9: BOOLEAN; + +ASSERT (a5); + +ASSERT (a0 OR (a1 AND (a2 OR (a3 AND (a4 AND (a5 AND (TRUE AND (a3 AND (a6 AND (a7 AND (a8 AND a9))))))))))); + +CHECKSAT; + +% EXIT: 10 + diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h index e71dcb41d..ccba0164a 100644 --- a/test/unit/prop/cnf_stream_white.h +++ b/test/unit/prop/cnf_stream_white.h @@ -55,7 +55,7 @@ public: d_addClauseCalled(false) { } - SatVariable newVar(bool theoryAtom) { + SatVariable newVar(bool theoryAtom, bool preRegister, bool canErase) { return d_nextVar++; } |