diff options
70 files changed, 2884 insertions, 1313 deletions
diff --git a/configure.ac b/configure.ac index 407b47b16..bdce30f28 100644 --- a/configure.ac +++ b/configure.ac @@ -2,8 +2,8 @@ # Process this file with autoconf to produce a configure script. m4_define(_CVC4_MAJOR, 1) dnl version (major) -m4_define(_CVC4_MINOR, 2) dnl version (minor) -m4_define(_CVC4_RELEASE, 1) dnl version (alpha) +m4_define(_CVC4_MINOR, 3) dnl version (minor) +m4_define(_CVC4_RELEASE, 0) dnl version (alpha) m4_define(_CVC4_EXTRAVERSION, [-prerelease]) dnl version (extra) m4_define(_CVC4_RELEASE_STRING, _CVC4_MAJOR[.]_CVC4_MINOR[]m4_if(_CVC4_RELEASE,[0],,[.]_CVC4_RELEASE)_CVC4_EXTRAVERSION) dnl version string diff --git a/contrib/run-script-casc24-fnt b/contrib/run-script-casc24-fnt new file mode 100755 index 000000000..2a10c5347 --- /dev/null +++ b/contrib/run-script-casc24-fnt @@ -0,0 +1,38 @@ +#!/bin/bash + +cvc4=./cvc4 +bench="$1" +let "to = $2 - 60" + +file=${bench##*/} +filename=${file%.*} + +# use: trywith [params..] +# to attempt a run. Only thing printed on stdout is "sat" or "unsat", in +# which case this run script terminates immediately. Otherwise, this +# function returns normally. +function trywith { + limit=$1; shift; + (ulimit -t "$limit";$cvc4 -L tptp --szs-compliant --no-checking --no-interactive --dump-models --produce-models "$@" $bench) 2>/dev/null | + (read result; + case "$result" in + sat) echo "% SZS Satisfiable for $filename"; + echo "% SZS output start FiniteModel for $filename"; + cat; + echo "% SZS output end FiniteModel for $filename"; + exit 0;; + unsat) echo "% SZS Unsatisfiable for $filename"; exit 0;; + conjecture-sat) echo "% SZS CounterSatisfiable for $filename"; + echo "% SZS output start FiniteModel for $filename"; + cat; + echo "% SZS output end FiniteModel for $filename"; + exit 0;; + conjecture-unsat) echo "% SZS Theorem for $filename"; exit 0;; + esac; exit 1) + if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi +} + +trywith 30 --finite-model-find --uf-ss-totality +trywith 30 --finite-model-find --decision=justification --fmf-fmc +trywith $to --finite-model-find --decision=justification +echo "% SZS GaveUp for $filename"
\ No newline at end of file diff --git a/contrib/run-script-casc24-fnt-no-models b/contrib/run-script-casc24-fnt-no-models new file mode 100755 index 000000000..a189c10bd --- /dev/null +++ b/contrib/run-script-casc24-fnt-no-models @@ -0,0 +1,36 @@ +#!/bin/bash + +cvc4=./cvc4 +bench="$1" +let "to = $2 - 60" + +file=${bench##*/} +filename=${file%.*} + +# use: trywith [params..] +# to attempt a run. Only thing printed on stdout is "sat" or "unsat", in +# which case this run script terminates immediately. Otherwise, this +# function returns normally. +function trywith { + result="$( ulimit -t "$1";shift;$cvc4 -L tptp --szs-compliant --no-checking --no-interactive "$@" $bench)" + case "$result" in + sat) echo "% SZS Satisfiable for $filename"; exit 0;; + unsat) echo "% SZS Unsatisfiable for $filename"; exit 0;; + conjecture-sat) echo "% SZS CounterSatisfiable for $filename"; exit 0;; + conjecture-unsat) echo "% SZS Theorem for $filename"; exit 0;; + esac +} +function finishwith { + result="$( $cvc4 -L tptp --szs-compliant --no-checking --no-interactive "$@" $bench)" + case "$result" in + sat) echo "% SZS Satisfiable for $filename"; exit 0;; + unsat) echo "% SZS Unsatisfiable for $filename"; exit 0;; + conjecture-sat) echo "% SZS CounterSatisfiable for $filename"; exit 0;; + conjecture-unsat) echo "% SZS Theorem for $filename"; exit 0;; + esac +} + +trywith 30 --finite-model-find --uf-ss-totality +trywith 30 --finite-model-find --decision=justification --fmf-fmc +trywith $to --finite-model-find --decision=justification +echo "% SZS GaveUp for $filename"
\ No newline at end of file diff --git a/contrib/run-script-casc24-fof b/contrib/run-script-casc24-fof new file mode 100755 index 000000000..940e26946 --- /dev/null +++ b/contrib/run-script-casc24-fof @@ -0,0 +1,37 @@ +#!/bin/bash + +cvc4=./cvc4 +bench="$1" +let "to = $2 - 75" + +file=${bench##*/} +filename=${file%.*} + +# use: trywith [params..] +# to attempt a run. Only thing printed on stdout is "sat" or "unsat", in +# which case this run script terminates immediately. Otherwise, this +# function returns normally. +function trywith { + result="$( ulimit -t "$1";shift;$cvc4 -L tptp --szs-compliant --no-checking --no-interactive "$@" $bench)" + case "$result" in + sat) echo "% SZS Satisfiable for $filename"; exit 0;; + unsat) echo "% SZS Unsatisfiable for $filename"; exit 0;; + conjecture-sat) echo "% SZS CounterSatisfiable for $filename"; exit 0;; + conjecture-unsat) echo "% SZS Theorem for $filename"; exit 0;; + esac +} +function finishwith { + result="$( $cvc4 -L tptp --szs-compliant --no-checking --no-interactive "$@" $bench)" + case "$result" in + sat) echo "% SZS Satisfiable for $filename"; exit 0;; + unsat) echo "% SZS Unsatisfiable for $filename"; exit 0;; + conjecture-sat) echo "% SZS CounterSatisfiable for $filename"; exit 0;; + conjecture-unsat) echo "% SZS Theorem for $filename"; exit 0;; + esac +} + +trywith 30 +trywith 15 --finite-model-find --fmf-inst-engine +trywith 30 --finite-model-find --decision=justification --fmf-fmc +trywith $to --decision=justification +echo "% SZS GaveUp for $filename"
\ No newline at end of file diff --git a/library_versions b/library_versions index c686e8f46..ad37ce67a 100644 --- a/library_versions +++ b/library_versions @@ -52,5 +52,6 @@ 1\.2-prerelease libcvc4:1:0:0 libcvc4parser:1:0:0 libcvc4compat:1:0:0 libcvc4bindings:1:0:0 1\.2 libcvc4:1:1:1 libcvc4parser:1:1:0 libcvc4compat:1:0:0 libcvc4bindings:1:0:0 1\.2\.1-prerelease libcvc4:1:1:1 libcvc4parser:1:1:0 libcvc4compat:1:0:0 libcvc4bindings:1:0:0 +1\.3-prerelease libcvc4:1:1:1 libcvc4parser:1:1:0 libcvc4compat:1:0:0 libcvc4bindings:1:0:0 # note: SmtEngine::setLogicString() exceptions have changed, bump library version on next release? # note: removed Parser::getDeclarationLevel(), added other interfaces diff --git a/src/decision/Makefile.am b/src/decision/Makefile.am index 6d49c6301..f75a17a69 100644 --- a/src/decision/Makefile.am +++ b/src/decision/Makefile.am @@ -12,9 +12,7 @@ libdecision_la_SOURCES = \ decision_engine.cpp \ decision_strategy.h \ justification_heuristic.h \ - justification_heuristic.cpp \ - relevancy.h \ - relevancy.cpp + justification_heuristic.cpp EXTRA_DIST = \ options_handlers.h diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp index f634a28d9..073a3ff6b 100644 --- a/src/decision/decision_engine.cpp +++ b/src/decision/decision_engine.cpp @@ -16,7 +16,6 @@ #include "decision/decision_engine.h" #include "decision/justification_heuristic.h" -#include "decision/relevancy.h" #include "expr/node.h" #include "decision/options.h" @@ -62,18 +61,6 @@ void DecisionEngine::init() enableStrategy(ds); d_needIteSkolemMap.push_back(ds); } - if(options::decisionMode() == decision::DECISION_STRATEGY_RELEVANCY) { - if(options::incrementalSolving()) { - Warning() << "Relevancy decision heuristic and incremental not supported together" - << std::endl; - return; // Currently not supported with incremental - } - RelevancyStrategy* ds = - new decision::Relevancy(this, d_satContext); - enableStrategy(ds); - d_needIteSkolemMap.push_back(ds); - d_relevancyStrategy = ds; - } } @@ -112,13 +99,6 @@ SatValue DecisionEngine::getPolarity(SatVariable var) } } - - - - - - - void DecisionEngine::addAssertions(const vector<Node> &assertions) { Assert(false); // doing this so that we revisit what to do @@ -146,15 +126,4 @@ void DecisionEngine::addAssertions(const vector<Node> &assertions, addAssertions(assertions, assertionsEnd, iteSkolemMap); } -// void DecisionEngine::addAssertion(Node n) -// { -// d_result = SAT_VALUE_UNKNOWN; -// if(needIteSkolemMap()) { -// d_assertions.push_back(n); -// } -// for(unsigned i = 0; i < d_needIteSkolemMap.size(); ++i) -// d_needIteSkolemMap[i]->notifyAssertionsAvailable(); -// } - - }/* CVC4 namespace */ diff --git a/src/decision/options b/src/decision/options index b86577e7b..5f89e9611 100644 --- a/src/decision/options +++ b/src/decision/options @@ -9,14 +9,6 @@ module DECISION "decision/options.h" Decision heuristics option decisionMode --decision=MODE decision::DecisionMode :handler CVC4::decision::stringToDecisionMode :default decision::DECISION_STRATEGY_INTERNAL :read-write :include "decision/decision_mode.h" :handler-include "decision/options_handlers.h" choose decision mode, see --decision=help -option decisionRelevancyLeaves bool -# permille = part per thousand -option decisionMaxRelTimeAsPermille --decision-budget=N "unsigned short" :read-write :predicate less_equal(1000L) :predicate CVC4::decision::checkDecisionBudget :predicate-include "decision/options_handlers.h" - impose a budget for relevancy heuristic which increases linearly with each decision. N between 0 and 1000. (default: 1000, no budget) -# if false, do justification stuff using relevancy.h -option decisionComputeRelevancy bool -# use the must be relevant -option decisionMustRelevancy bool # only use DE to determine when to stop, not to make decisions option decisionStopOnly bool diff --git a/src/decision/options_handlers.h b/src/decision/options_handlers.h index 05d975ef1..44a623970 100644 --- a/src/decision/options_handlers.h +++ b/src/decision/options_handlers.h @@ -37,31 +37,8 @@ justification\n\ justification-stoponly\n\ + Use the justification heuristic only to stop early, not for decisions\n\ "; -/** Under-development options, commenting out from help for the release */ -/* -\n\ -relevancy\n\ -+ Under development may-relevancy\n\ -\n\ -relevancy-leaves\n\ -+ May-relevancy, but decide only on leaves\n\ -\n\ -Developer modes:\n\ -\n\ -justification-rel\n\ -+ Use the relevancy code to do the justification stuff\n\ -+ (This should do exact same thing as justification)\n\ -\n\ -justification-must\n\ -+ Start deciding on literals close to root instead of those\n\ -+ near leaves (don't expect it to work well) [Unimplemented]\n\ -";*/ inline DecisionMode stringToDecisionMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - options::decisionRelevancyLeaves.set(false); - options::decisionMaxRelTimeAsPermille.set(1000); - options::decisionComputeRelevancy.set(true); - options::decisionMustRelevancy.set(false); options::decisionStopOnly.set(false); if(optarg == "internal") { @@ -71,25 +48,6 @@ inline DecisionMode stringToDecisionMode(std::string option, std::string optarg, } else if(optarg == "justification-stoponly") { options::decisionStopOnly.set(true); return DECISION_STRATEGY_JUSTIFICATION; - } else if(optarg == "relevancy") { - options::decisionRelevancyLeaves.set(false); - return DECISION_STRATEGY_RELEVANCY; - } else if(optarg == "relevancy-leaves") { - options::decisionRelevancyLeaves.set(true); - Trace("options") << "version is " << options::version() << std::endl; - return DECISION_STRATEGY_RELEVANCY; - } else if(optarg == "justification-rel") { - // relevancyLeaves : irrelevant - // maxRelTimeAsPermille : irrelevant - options::decisionComputeRelevancy.set(false); - options::decisionMustRelevancy.set(false); - return DECISION_STRATEGY_RELEVANCY; - } else if(optarg == "justification-must") { - // relevancyLeaves : irrelevant - // maxRelTimeAsPermille : irrelevant - options::decisionComputeRelevancy.set(false); - options::decisionMustRelevancy.set(true); - return DECISION_STRATEGY_RELEVANCY; } else if(optarg == "help") { puts(decisionModeHelp.c_str()); exit(1); @@ -99,14 +57,6 @@ inline DecisionMode stringToDecisionMode(std::string option, std::string optarg, } } -inline void checkDecisionBudget(std::string option, unsigned short budget, SmtEngine* smt) throw(OptionException) { - if(budget == 0) { - Warning() << "Decision budget is 0. Consider using internal decision heuristic and " - << std::endl << " removing this option." << std::endl; - - } -} - inline DecisionWeightInternal stringToDecisionWeightInternal(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { if(optarg == "off") return DECISION_WEIGHT_INTERNAL_OFF; diff --git a/src/decision/relevancy.cpp b/src/decision/relevancy.cpp deleted file mode 100644 index f83e238d4..000000000 --- a/src/decision/relevancy.cpp +++ /dev/null @@ -1,379 +0,0 @@ -/********************* */ -/*! \file relevancy.cpp - ** \verbatim - ** Original author: Kshitij Bansal - ** Major contributors: none - ** Minor contributors (to current version): Dejan Jovanovic, Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Justification heuristic for decision making - ** - ** A ATGP-inspired justification-based decision heuristic. See - ** [insert reference] for more details. This code is, or not, based - ** on the CVC3 implementation of the same heuristic -- note below. - ** - ** It needs access to the simplified but non-clausal formula. - **/ -/*****************************************************************************/ - -#include "relevancy.h" - -#include "expr/node_manager.h" -#include "expr/kind.h" -#include "theory/rewriter.h" -#include "util/ite_removal.h" - -// Relevancy stuff - -const double Relevancy::secondsPerDecision = 0.001; -const double Relevancy::secondsPerExpense = 1e-7; -const double Relevancy::EPS = 1e-9; - - -void Relevancy::setJustified(TNode n) -{ - Debug("decision") << " marking [" << n.getId() << "]"<< n << "as justified" << std::endl; - d_justified.insert(n); - if(options::decisionComputeRelevancy()) { - d_relevancy[n] = d_maxRelevancy[n]; - updateRelevancy(n); - } -} - -bool Relevancy::checkJustified(TNode n) -{ - return d_justified.find(n) != d_justified.end(); -} - -SatValue Relevancy::tryGetSatValue(Node n) -{ - Debug("decision") << " " << n << " has sat value " << " "; - if(d_decisionEngine->hasSatLiteral(n) ) { - Debug("decision") << d_decisionEngine->getSatValue(n) << std::endl; - return d_decisionEngine->getSatValue(n); - } else { - Debug("decision") << "NO SAT LITERAL" << std::endl; - return SAT_VALUE_UNKNOWN; - }//end of else -} - -void Relevancy::computeITEs(TNode n, IteList &l) -{ - Debug("jh-ite") << " computeITEs( " << n << ", &l)\n"; - for(unsigned i=0; i<n.getNumChildren(); ++i) { - SkolemMap::iterator it2 = d_iteAssertions.find(n[i]); - if(it2 != d_iteAssertions.end()) - l.push_back(it2->second); - computeITEs(n[i], l); - } -} - -const Relevancy::IteList& Relevancy::getITEs(TNode n) -{ - IteCache::iterator it = d_iteCache.find(n); - if(it != d_iteCache.end()) { - return it->second; - } else { - // Compute the list of ITEs - // TODO: optimize by avoiding multiple lookup for d_iteCache[n] - d_iteCache[n] = vector<TNode>(); - computeITEs(n, d_iteCache[n]); - return d_iteCache[n]; - } -} - -bool Relevancy::findSplitterRec(TNode node, - SatValue desiredVal) -{ - Trace("decision") - << "findSplitterRec([" << node.getId() << "]" << node << ", " - << desiredVal << ", .. )" << std::endl; - - ++d_expense; - - /* Handle NOT as a special case */ - while (node.getKind() == kind::NOT) { - desiredVal = invertValue(desiredVal); - node = node[0]; - } - - /* Avoid infinite loops */ - if(d_visited.find(node) != d_visited.end()) { - Debug("decision") << " node repeated. kind was " << node.getKind() << std::endl; - Assert(false); - Assert(node.getKind() == kind::ITE); - return false; - } - - /* Base case */ - if(checkJustified(node)) { - return false; - } - - /** - * If we have already explored the subtree for some desiredVal, we - * skip this and continue exploring the rest - */ - if(d_polarityCache.find(node) == d_polarityCache.end()) { - d_polarityCache[node] = desiredVal; - } else { - Assert(d_multipleBacktrace || options::decisionComputeRelevancy()); - return true; - } - - d_visited.insert(node); - -#if defined CVC4_ASSERTIONS || defined CVC4_TRACING - // We don't always have a sat literal, so remember that. Will need - // it for some assertions we make. - bool litPresent = d_decisionEngine->hasSatLiteral(node); - if(Trace.isOn("decision")) { - if(!litPresent) { - Trace("decision") << "no sat literal for this node" << std::endl; - } - } - //Assert(litPresent); -- fails -#endif - - // Get value of sat literal for the node, if there is one - SatValue litVal = tryGetSatValue(node); - - /* You'd better know what you want */ - Assert(desiredVal != SAT_VALUE_UNKNOWN, "expected known value"); - - /* Good luck, hope you can get what you want */ - Assert(litVal == desiredVal || litVal == SAT_VALUE_UNKNOWN, - "invariant violated"); - - /* What type of node is this */ - Kind k = node.getKind(); - theory::TheoryId tId = theory::kindToTheoryId(k); - - /* Some debugging stuff */ - Trace("jh-findSplitterRec") << "kind = " << k << std::endl; - Trace("jh-findSplitterRec") << "theoryId = " << tId << std::endl; - Trace("jh-findSplitterRec") << "node = " << node << std::endl; - Trace("jh-findSplitterRec") << "litVal = " << litVal << std::endl; - - /** - * If not in theory of booleans, and not a "boolean" EQUAL (IFF), - * then check if this is something to split-on. - */ - if(tId != theory::THEORY_BOOL - // && !(k == kind::EQUAL && node[0].getType().isBoolean()) - ) { - - // if node has embedded ites -- which currently happens iff it got - // replaced during ite removal -- then try to resolve that first - const IteList& l = getITEs(node); - Debug("jh-ite") << " ite size = " << l.size() << std::endl; - for(unsigned i = 0; i < l.size(); ++i) { - Assert(l[i].getKind() == kind::ITE, "Expected ITE"); - Debug("jh-ite") << " i = " << i - << " l[i] = " << l[i] << std::endl; - if(d_visited.find(node) != d_visited.end() ) continue; - if(findSplitterRec(l[i], SAT_VALUE_TRUE)) { - d_visited.erase(node); - return true; - } - } - Debug("jh-ite") << " ite done " << l.size() << std::endl; - - if(litVal != SAT_VALUE_UNKNOWN) { - d_visited.erase(node); - setJustified(node); - return false; - } else { - /* if(not d_decisionEngine->hasSatLiteral(node)) - throw GiveUpException(); */ - Assert(d_decisionEngine->hasSatLiteral(node)); - SatVariable v = d_decisionEngine->getSatLiteral(node).getSatVariable(); - *d_curDecision = SatLiteral(v, desiredVal != SAT_VALUE_TRUE ); - Trace("decision") << "decision " << *d_curDecision << std::endl; - Trace("decision") << "Found something to split. Glad to be able to serve you." << std::endl; - d_visited.erase(node); - return true; - } - } - - bool ret = false; - SatValue flipCaseVal = SAT_VALUE_FALSE; - switch (k) { - - case kind::CONST_BOOLEAN: - Assert(node.getConst<bool>() == false || desiredVal == SAT_VALUE_TRUE); - Assert(node.getConst<bool>() == true || desiredVal == SAT_VALUE_FALSE); - break; - - case kind::AND: - if (desiredVal == SAT_VALUE_FALSE) ret = handleOrTrue(node, SAT_VALUE_FALSE); - else ret = handleOrFalse(node, SAT_VALUE_TRUE); - break; - - case kind::OR: - if (desiredVal == SAT_VALUE_FALSE) ret = handleOrFalse(node, SAT_VALUE_FALSE); - else ret = handleOrTrue(node, SAT_VALUE_TRUE); - break; - - case kind::IMPLIES: - Assert(node.getNumChildren() == 2, "Expected 2 fanins"); - if (desiredVal == SAT_VALUE_FALSE) { - ret = findSplitterRec(node[0], SAT_VALUE_TRUE); - if(ret) break; - ret = findSplitterRec(node[1], SAT_VALUE_FALSE); - break; - } - else { - if (tryGetSatValue(node[0]) != SAT_VALUE_TRUE) { - ret = findSplitterRec(node[0], SAT_VALUE_FALSE); - //if(!ret || !d_multipleBacktrace) - break; - } - if (tryGetSatValue(node[1]) != SAT_VALUE_FALSE) { - ret = findSplitterRec(node[1], SAT_VALUE_TRUE); - break; - } - Assert(d_multipleBacktrace, "No controlling input found (3)"); - } - break; - - case kind::XOR: - flipCaseVal = SAT_VALUE_TRUE; - case kind::IFF: { - SatValue val = tryGetSatValue(node[0]); - if (val != SAT_VALUE_UNKNOWN) { - ret = findSplitterRec(node[0], val); - if (ret) break; - if (desiredVal == flipCaseVal) val = invertValue(val); - ret = findSplitterRec(node[1], val); - } - else { - val = tryGetSatValue(node[1]); - if (val == SAT_VALUE_UNKNOWN) val = SAT_VALUE_FALSE; - if (desiredVal == flipCaseVal) val = invertValue(val); - ret = findSplitterRec(node[0], val); - if(ret) break; - Assert(false, "Unable to find controlling input (4)"); - } - break; - } - - case kind::ITE: - ret = handleITE(node, desiredVal); - break; - - default: - Assert(false, "Unexpected Boolean operator"); - break; - }//end of switch(k) - - d_visited.erase(node); - if(ret == false) { - Assert(litPresent == false || litVal == desiredVal, - "Output should be justified"); - setJustified(node); - } - return ret; - - Unreachable(); -}/* findRecSplit method */ - -bool Relevancy::handleOrFalse(TNode node, SatValue desiredVal) { - Debug("jh-findSplitterRec") << " handleOrFalse (" << node << ", " - << desiredVal << std::endl; - - Assert( (node.getKind() == kind::AND and desiredVal == SAT_VALUE_TRUE) or - (node.getKind() == kind::OR and desiredVal == SAT_VALUE_FALSE) ); - - int n = node.getNumChildren(); - bool ret = false; - for(int i = 0; i < n; ++i) { - if (findSplitterRec(node[i], desiredVal)) { - if(!options::decisionComputeRelevancy()) - return true; - else - ret = true; - } - } - return ret; -} - -bool Relevancy::handleOrTrue(TNode node, SatValue desiredVal) { - Debug("jh-findSplitterRec") << " handleOrTrue (" << node << ", " - << desiredVal << std::endl; - - Assert( (node.getKind() == kind::AND and desiredVal == SAT_VALUE_FALSE) or - (node.getKind() == kind::OR and desiredVal == SAT_VALUE_TRUE) ); - - int n = node.getNumChildren(); - SatValue desiredValInverted = invertValue(desiredVal); - for(int i = 0; i < n; ++i) { - if ( tryGetSatValue(node[i]) != desiredValInverted ) { - // PRE RELEVANCY return findSplitterRec(node[i], desiredVal); - bool ret = findSplitterRec(node[i], desiredVal); - if(ret) { - // Splitter could be found... so can't justify this node - if(!d_multipleBacktrace) - return true; - } - else { - // Splitter couldn't be found... should be justified - return false; - } - } - } - // Multiple backtrace is on, so must have reached here because - // everything had splitter - if(d_multipleBacktrace) return true; - - if(Debug.isOn("jh-findSplitterRec")) { - Debug("jh-findSplitterRec") << " * ** " << std::endl; - Debug("jh-findSplitterRec") << node.getKind() << " " - << node << std::endl; - for(unsigned i = 0; i < node.getNumChildren(); ++i) - Debug("jh-findSplitterRec") << "child: " << tryGetSatValue(node[i]) - << std::endl; - Debug("jh-findSplitterRec") << "node: " << tryGetSatValue(node) - << std::endl; - } - Assert(false, "No controlling input found"); - return false; -} - -bool Relevancy::handleITE(TNode node, SatValue desiredVal) -{ - Debug("jh-findSplitterRec") << " handleITE (" << node << ", " - << desiredVal << std::endl; - - //[0]: if, [1]: then, [2]: else - SatValue ifVal = tryGetSatValue(node[0]); - if (ifVal == SAT_VALUE_UNKNOWN) { - - // are we better off trying false? if not, try true - SatValue ifDesiredVal = - (tryGetSatValue(node[2]) == desiredVal || - tryGetSatValue(node[1]) == invertValue(desiredVal)) - ? SAT_VALUE_FALSE : SAT_VALUE_TRUE; - - if(findSplitterRec(node[0], ifDesiredVal)) return true; - - Assert(false, "No controlling input found (6)"); - } else { - - // Try to justify 'if' - if(findSplitterRec(node[0], ifVal)) return true; - - // If that was successful, we need to go into only one of 'then' - // or 'else' - int ch = (ifVal == SAT_VALUE_TRUE) ? 1 : 2; - int chVal = tryGetSatValue(node[ch]); - if( (chVal == SAT_VALUE_UNKNOWN || chVal == desiredVal) && - findSplitterRec(node[ch], desiredVal) ) { - return true; - } - }// else (...ifVal...) - return false; -}//handleITE diff --git a/src/decision/relevancy.h b/src/decision/relevancy.h deleted file mode 100644 index fd16eb0cc..000000000 --- a/src/decision/relevancy.h +++ /dev/null @@ -1,421 +0,0 @@ -/********************* */ -/*! \file relevancy.h - ** \verbatim - ** Original author: Kshitij Bansal - ** Major contributors: none - ** Minor contributors (to current version): Tim King, Dejan Jovanovic, Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Justification heuristic for decision making - ** - ** A ATGP-inspired justification-based decision heuristic. See - ** [insert reference] for more details. This code is, or not, based - ** on the CVC3 implementation of the same heuristic. - ** - ** It needs access to the simplified but non-clausal formula. - ** - ** Relevancy - ** --------- - ** - ** This class also currently computes the may-relevancy of a node - ** - ** A node is may-relevant if there is a path from the root of the - ** formula to the node such that no node on the path is justified. As - ** contrapositive, a node is not relevant (with the may-notion) if all - ** path from the root to the node go through a justified node. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__DECISION__RELEVANCY -#define __CVC4__DECISION__RELEVANCY - -#include "decision_engine.h" -#include "decision_strategy.h" -#include "decision/options.h" - -#include "context/cdhashset.h" -#include "context/cdhashmap.h" -#include "expr/node.h" -#include "prop/sat_solver_types.h" - -namespace CVC4 { - -namespace decision { - -class RelGiveUpException : public Exception { -public: - RelGiveUpException() : - Exception("relevancy: giving up") { - } -};/* class GiveUpException */ - -class Relevancy : public RelevancyStrategy { - typedef std::vector<TNode> IteList; - typedef hash_map<TNode,IteList,TNodeHashFunction> IteCache; - typedef hash_map<TNode,TNode,TNodeHashFunction> SkolemMap; - typedef hash_map<TNode,SatValue,TNodeHashFunction> PolarityCache; - - // being 'justified' is monotonic with respect to decisions - context::CDHashSet<Node, NodeHashFunction> d_justified; - context::CDO<unsigned> d_prvsIndex; - - IntStat d_helfulness; - IntStat d_polqueries; - IntStat d_polhelp; - IntStat d_giveup; - IntStat d_expense; /* Total number of nodes considered over - all calls to the findSplitter function */ - TimerStat d_timestat; - - /** - * A copy of the assertions that need to be justified - * directly. Doesn't have ones introduced during during ITE-removal. - */ - std::vector<TNode> d_assertions; - //TNode is fine since decisionEngine has them too - - /** map from ite-rewrite skolem to a boolean-ite assertion */ - SkolemMap d_iteAssertions; - // 'key' being TNode is fine since if a skolem didn't exist anywhere, - // we won't look it up. as for 'value', same reason as d_assertions - - /** Cache for ITE skolems present in a atomic formula */ - IteCache d_iteCache; - - /** - * This is used to prevent infinite loop when trying to find a - * splitter. Can happen when exploring assertion corresponding to a - * term-ITE. - */ - hash_set<TNode,TNodeHashFunction> d_visited; - - /** - * May-relevancy of a node is an integer. For a node n, it becomes - * irrelevant when d_maxRelevancy[n] = d_relevancy[n] - */ - hash_map<TNode,int,TNodeHashFunction> d_maxRelevancy; - context::CDHashMap<TNode,int,TNodeHashFunction> d_relevancy; - PolarityCache d_polarityCache; - - /** **** * * *** * * OPTIONS *** * * ** * * **** */ - - /** - * do we do "multiple-backtrace" to try to justify a node - */ - bool d_multipleBacktrace; - //bool d_computeRelevancy; // are we in a mode where we compute relevancy? - - static const double secondsPerDecision; - static const double secondsPerExpense; - static const double EPS; - - /** Maximum time this algorithm should spent as part of whole algorithm */ - double d_maxTimeAsPercentageOfTotalTime; - - /** current decision for the recursive call */ - SatLiteral* d_curDecision; -public: - Relevancy(CVC4::DecisionEngine* de, context::Context *c): - RelevancyStrategy(de, c), - d_justified(c), - d_prvsIndex(c, 0), - d_helfulness("decision::rel::preventedDecisions", 0), - d_polqueries("decision::rel::polarityQueries", 0), - d_polhelp("decision::rel::polarityHelp", 0), - d_giveup("decision::rel::giveup", 0), - d_expense("decision::rel::expense", 0), - d_timestat("decision::rel::time"), - d_relevancy(c), - d_multipleBacktrace(options::decisionComputeRelevancy()), - // d_computeRelevancy(decOpt.computeRelevancy), - d_maxTimeAsPercentageOfTotalTime(options::decisionMaxRelTimeAsPermille()*1.0/10.0), - d_curDecision(NULL) - { - Warning() << "There are known bugs in this Relevancy code which we know" - << "how to fix (but haven't yet)." << std::endl - << "Please bug kshitij if you wish to use." << std::endl; - - StatisticsRegistry::registerStat(&d_helfulness); - StatisticsRegistry::registerStat(&d_polqueries); - StatisticsRegistry::registerStat(&d_polhelp); - StatisticsRegistry::registerStat(&d_giveup); - StatisticsRegistry::registerStat(&d_expense); - StatisticsRegistry::registerStat(&d_timestat); - Trace("decision") << "relevancy enabled with" << std::endl; - Trace("decision") << " * computeRelevancy: " << (options::decisionComputeRelevancy() ? "on" : "off") - << std::endl; - Trace("decision") << " * relevancyLeaves: " << (options::decisionRelevancyLeaves() ? "on" : "off") - << std::endl; - Trace("decision") << " * mustRelevancy [unimplemented]: " << (options::decisionMustRelevancy() ? "on" : "off") - << std::endl; - } - ~Relevancy() { - StatisticsRegistry::unregisterStat(&d_helfulness); - StatisticsRegistry::unregisterStat(&d_polqueries); - StatisticsRegistry::unregisterStat(&d_polhelp); - StatisticsRegistry::unregisterStat(&d_giveup); - StatisticsRegistry::unregisterStat(&d_expense); - StatisticsRegistry::unregisterStat(&d_timestat); - } - prop::SatLiteral getNext(bool &stopSearch) { - Debug("decision") << std::endl; - Trace("decision") << "Relevancy::getNext()" << std::endl; - TimerStat::CodeTimer codeTimer(d_timestat); - - if( d_maxTimeAsPercentageOfTotalTime < 100.0 - EPS && - double(d_polqueries.getData())*secondsPerDecision < - d_maxTimeAsPercentageOfTotalTime*double(d_expense.getData())*secondsPerExpense - ) { - ++d_giveup; - return undefSatLiteral; - } - - d_visited.clear(); - d_polarityCache.clear(); - - for(unsigned i = d_prvsIndex; i < d_assertions.size(); ++i) { - Trace("decision") << d_assertions[i] << std::endl; - - // Sanity check: if it was false, aren't we inconsistent? - Assert( tryGetSatValue(d_assertions[i]) != SAT_VALUE_FALSE); - - SatValue desiredVal = SAT_VALUE_TRUE; - SatLiteral litDecision = findSplitter(d_assertions[i], desiredVal); - - if(!options::decisionComputeRelevancy() && litDecision != undefSatLiteral) { - d_prvsIndex = i; - return litDecision; - } - } - - if(options::decisionComputeRelevancy()) return undefSatLiteral; - - Trace("decision") << "jh: Nothing to split on " << std::endl; - -#if defined CVC4_ASSERTIONS || defined CVC4_DEBUG - bool alljustified = true; - for(unsigned i = 0 ; i < d_assertions.size() && alljustified ; ++i) { - TNode curass = d_assertions[i]; - while(curass.getKind() == kind::NOT) - curass = curass[0]; - alljustified &= checkJustified(curass); - - if(Debug.isOn("decision")) { - if(!checkJustified(curass)) - Debug("decision") << "****** Not justified [i="<<i<<"]: " - << d_assertions[i] << std::endl; - } - } - Assert(alljustified); -#endif - - // SAT solver can stop... - stopSearch = true; - d_decisionEngine->setResult(SAT_VALUE_TRUE); - return prop::undefSatLiteral; - } - - void addAssertions(const std::vector<Node> &assertions, - unsigned assertionsEnd, - IteSkolemMap iteSkolemMap) { - Trace("decision") - << "Relevancy::addAssertions()" - << " size = " << assertions.size() - << " assertionsEnd = " << assertionsEnd - << std::endl; - - // Save mapping between ite skolems and ite assertions - for(IteSkolemMap::iterator i = iteSkolemMap.begin(); - i != iteSkolemMap.end(); ++i) { - Assert(i->second >= assertionsEnd && i->second < assertions.size()); - Debug("jh-ite") << " jh-ite: " << (i->first) << " maps to " - << assertions[(i->second)] << std::endl; - d_iteAssertions[i->first] = assertions[i->second]; - } - - // Save the 'real' assertions locally - for(unsigned i = 0; i < assertionsEnd; ++i) { - d_assertions.push_back(assertions[i]); - d_visited.clear(); - if(options::decisionComputeRelevancy()) increaseMaxRelevancy(assertions[i]); - d_visited.clear(); - } - - } - - bool isRelevant(TNode n) { - Trace("decision") << "isRelevant(" << n << "): "; - - if(Debug.isOn("decision")) { - if(d_maxRelevancy.find(n) == d_maxRelevancy.end()) { - // we are becuase of not getting information about literals - // created using newLiteral command... need to figure how to - // handle that - Message() << "isRelevant: WARNING: didn't find node when we should had" << std::endl; - } - } - - if(d_maxRelevancy.find(n) == d_maxRelevancy.end()) { - Trace("decision") << "yes [not found in db]" << std::endl; - return true; - } - - if(options::decisionRelevancyLeaves() && !isAtomicFormula(n)) { - Trace("decision") << "no [not a leaf]" << std::endl; - return false; - } - - Trace("decision") << (d_maxRelevancy[n] == d_relevancy[n] ? "no":"yes") - << std::endl; - - Debug("decision") << " maxRel: " << (d_maxRelevancy[n] ) - << " rel: " << d_relevancy[n].get() << std::endl; - // Assert(d_maxRelevancy.find(n) != d_maxRelevancy.end()); - Assert(0 <= d_relevancy[n] && d_relevancy[n] <= d_maxRelevancy[n]); - - if(d_maxRelevancy[n] == d_relevancy[n]) { - ++d_helfulness; // preventedDecisions - return false; - } else { - return true; - } - } - - SatValue getPolarity(TNode n) { - Trace("decision") << "getPolarity([" << n.getId() << "]" << n << "): "; - Assert(n.getKind() != kind::NOT); - ++d_polqueries; - PolarityCache::iterator it = d_polarityCache.find(n); - if(it == d_polarityCache.end()) { - Trace("decision") << "don't know" << std::endl; - return SAT_VALUE_UNKNOWN; - } else { - ++d_polhelp; - Trace("decision") << it->second << std::endl; - return it->second; - } - } - - /* Compute justified */ - /*bool computeJustified() { - - }*/ -private: - SatLiteral findSplitter(TNode node, SatValue desiredVal) - { - bool ret; - SatLiteral litDecision; - try { - // init - d_curDecision = &litDecision; - - // solve - ret = findSplitterRec(node, desiredVal); - - // post - d_curDecision = NULL; - }catch(RelGiveUpException &e) { - return prop::undefSatLiteral; - } - if(ret == true) { - Trace("decision") << "Yippee!!" << std::endl; - return litDecision; - } else { - return undefSatLiteral; - } - } - - /** - * Do all the hardwork. - * Return 'true' if the node cannot be justfied, 'false' it it can be. - * Sets 'd_curDecision' if unable to justify (depending on the mode) - * If 'd_computeRelevancy' is on does multiple backtrace - */ - bool findSplitterRec(TNode node, SatValue value); - // Functions to make findSplitterRec modular... - bool handleOrFalse(TNode node, SatValue desiredVal); - bool handleOrTrue(TNode node, SatValue desiredVal); - bool handleITE(TNode node, SatValue desiredVal); - - /* Helper functions */ - void setJustified(TNode); - bool checkJustified(TNode); - - /* If literal exists corresponding to the node return - that. Otherwise an UNKNOWN */ - SatValue tryGetSatValue(Node n); - - /* Get list of all term-ITEs for the atomic formula v */ - const Relevancy::IteList& getITEs(TNode n); - - /* Compute all term-ITEs in a node recursively */ - void computeITEs(TNode n, IteList &l); - - /* Checks whether something is an atomic formula or not */ - bool isAtomicFormula(TNode n) { - return theory::kindToTheoryId(n.getKind()) != theory::THEORY_BOOL; - } - - /** Recursively increase relevancies */ - void updateRelevancy(TNode n) { - if(d_visited.find(n) != d_visited.end()) return; - - Assert(d_relevancy[n] <= d_maxRelevancy[n]); - - if(d_relevancy[n] != d_maxRelevancy[n]) - return; - - d_visited.insert(n); - if(isAtomicFormula(n)) { - const IteList& l = getITEs(n); - for(unsigned i = 0; i < l.size(); ++i) { - if(d_visited.find(l[i]) == d_visited.end()) continue; - d_relevancy[l[i]] = d_relevancy[l[i]] + 1; - updateRelevancy(l[i]); - } - } else { - for(unsigned i = 0; i < n.getNumChildren(); ++i) { - if(d_visited.find(n[i]) == d_visited.end()) continue; - d_relevancy[n[i]] = d_relevancy[n[i]] + 1; - updateRelevancy(n[i]); - } - } - d_visited.erase(n); - } - - /* */ - void increaseMaxRelevancy(TNode n) { - - Debug("decision") - << "increaseMaxRelevancy([" << n.getId() << "]" << n << ")" - << std::endl; - - d_maxRelevancy[n]++; - - // don't update children multiple times - if(d_visited.find(n) != d_visited.end()) return; - - d_visited.insert(n); - // Part to make the recursive call - if(isAtomicFormula(n)) { - const IteList& l = getITEs(n); - for(unsigned i = 0; i < l.size(); ++i) - if(d_visited.find(l[i]) == d_visited.end()) - increaseMaxRelevancy(l[i]); - } else { - for(unsigned i = 0; i < n.getNumChildren(); ++i) - increaseMaxRelevancy(n[i]); - } //else (...atomic formula...) - } - -};/* class Relevancy */ - -}/* namespace decision */ - -}/* namespace CVC4 */ - -#endif /* __CVC4__DECISION__RELEVANCY */ diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index f1742b549..556e51216 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -19,6 +19,8 @@ #include "main/main.h" +#include "smt/options.h" + namespace CVC4 { namespace main { @@ -64,6 +66,17 @@ bool CommandExecutor::doCommandSingleton(Command *cmd) } else { status = smtEngineInvoke(&d_smtEngine, cmd, NULL); } + //dump the model if option is set + if(status && d_options[options::produceModels] && d_options[options::dumpModels]) { + CheckSatCommand *cs = dynamic_cast<CheckSatCommand*>(cmd); + if(cs != NULL) { + if(cs->getResult().asSatisfiabilityResult().isSat() == Result::SAT || + (cs->getResult().isUnknown() && cs->getResult().whyUnknown() == Result::INCOMPLETE) ){ + Command * gm = new GetModelCommand; + status = doCommandSingleton(gm); + } + } + } return status; } diff --git a/src/parser/options b/src/parser/options index beae09823..b3e69a992 100644 --- a/src/parser/options +++ b/src/parser/options @@ -14,4 +14,7 @@ option memoryMap --mmap bool option semanticChecks /--no-checking bool :default DO_SEMANTIC_CHECKS_BY_DEFAULT :link /--no-type-checking disable ALL semantic checks, including type checks +option szsCompliant --szs-compliant bool :default false + temporary support for szs ontolotogy, print if conjecture is found + endmodule diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index 721337c9e..e1e4053ac 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -89,7 +89,11 @@ Parser* ParserBuilder::build() parser = new Smt2(d_exprManager, input, d_strictMode, d_parseOnly); break; case language::input::LANG_TPTP: - parser = new Tptp(d_exprManager, input, d_strictMode, d_parseOnly); + { + Tptp * tparser = new Tptp(d_exprManager, input, d_strictMode, d_parseOnly); + tparser->d_szsCompliant = d_szsCompliant; + parser = tparser; + } break; default: parser = new Parser(d_exprManager, input, d_strictMode, d_parseOnly); @@ -141,6 +145,7 @@ ParserBuilder& ParserBuilder::withParseOnly(bool flag) { } ParserBuilder& ParserBuilder::withOptions(const Options& options) { + d_szsCompliant = options[options::szsCompliant]; return withInputLanguage(options[options::inputLanguage]) .withMmap(options[options::memoryMap]) diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h index 75e2b4fbe..607547beb 100644 --- a/src/parser/parser_builder.h +++ b/src/parser/parser_builder.h @@ -77,6 +77,9 @@ class CVC4_PUBLIC ParserBuilder { /** Are we parsing only? */ bool d_parseOnly; + /** hack for szs compliance */ + bool d_szsCompliant; + /** Initialize this parser builder */ void init(ExprManager* exprManager, const std::string& filename); diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index ee7ee4c61..ab4ea14c4 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -52,6 +52,7 @@ Tptp::Tptp(ExprManager* exprManager, Input* input, bool strictMode, bool parseOn d_tptpDir.append("/"); } } + d_hasConjecture = false; } void Tptp::addTheory(Theory theory) { diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h index 6b7adbbf7..cea246282 100644 --- a/src/parser/tptp/tptp.h +++ b/src/parser/tptp/tptp.h @@ -24,6 +24,7 @@ #include "util/hash.h" #include <ext/hash_set> #include <cassert> +#include "parser/options.h" namespace CVC4 { @@ -49,6 +50,11 @@ class Tptp : public Parser { // empty if none could be determined std::string d_tptpDir; + //hack to make output SZS ontology-compliant + bool d_hasConjecture; + // hack for szs compliance + bool d_szsCompliant; + public: bool cnf; //in a cnf formula @@ -181,6 +187,13 @@ inline void Tptp::makeApplication(Expr & expr, std::string & name, }; inline Command* Tptp::makeCommand(FormulaRole fr, Expr & expr){ + //hack for SZS ontology compliance + if(d_szsCompliant && (fr==FR_NEGATED_CONJECTURE || fr==FR_CONJECTURE)){ + if( !d_hasConjecture ){ + d_hasConjecture = true; + std::cout << "conjecture-"; + } + } switch(fr){ case FR_AXIOM: case FR_HYPOTHESIS: diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index c59df6269..a2fe96271 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -214,7 +214,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, bool stillNeedToPrintParams = true; // operator - if(n.getNumChildren() != 0) out << '('; + if(n.getNumChildren() != 0 && n.getKind()!=kind::INST_PATTERN_LIST) out << '('; switch(Kind k = n.getKind()) { // builtin theory case kind::APPLY: break; @@ -312,12 +312,29 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, break; // quantifiers - case kind::FORALL: out << "forall "; break; - case kind::EXISTS: out << "exists "; break; + case kind::FORALL: + case kind::EXISTS: + if( k==kind::FORALL ){ + out << "forall "; + }else{ + out << "exists "; + } + for( unsigned i=0; i<2; i++) { + out << n[i] << " "; + if( i==0 && n.getNumChildren()==3 ){ + out << "(! "; + } + } + if( n.getNumChildren()==3 ){ + out << n[2]; + out << ")"; + } + out << ")"; + return; + break; case kind::BOUND_VAR_LIST: // the left parenthesis is already printed (before the switch) - for(TNode::iterator i = n.begin(), - iend = n.end(); + for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ) { out << '('; toStream(out, (*i), toDepth < 0 ? toDepth : toDepth - 1, types); @@ -334,8 +351,13 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, out << ')'; return; case kind::INST_PATTERN: + break; case kind::INST_PATTERN_LIST: // TODO user patterns + for(unsigned i=0; i<n.getNumChildren(); i++) { + out << ":pattern " << n[i]; + } + return; break; default: diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp index d6e493c8d..5f03ef5cf 100644 --- a/src/proof/cnf_proof.cpp +++ b/src/proof/cnf_proof.cpp @@ -19,8 +19,8 @@ using namespace CVC4::prop; namespace CVC4 { + CnfProof::CnfProof(CnfStream* stream) : d_cnfStream(stream) {} - } /* CVC4 namespace */ diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h index c265e46df..984dc76c6 100644 --- a/src/proof/cnf_proof.h +++ b/src/proof/cnf_proof.h @@ -17,7 +17,7 @@ **/ #include "cvc4_private.h" - +#include "util/proof.h" #ifndef __CVC4__CNF_PROOF_H #define __CVC4__CNF_PROOF_H diff --git a/src/proof/sat_proof.cpp b/src/proof/sat_proof.cpp index df695c2d1..82478464f 100644 --- a/src/proof/sat_proof.cpp +++ b/src/proof/sat_proof.cpp @@ -173,7 +173,10 @@ SatProof::SatProof(Minisat::Solver* solver, bool checkRes) : d_emptyClauseId(-1), d_nullId(-2), d_temp_clauseId(), - d_temp_idClause() + d_temp_idClause(), + d_unitConflictId(), + d_storedUnitConflict(false), + d_atomToVar() { d_proxy = new ProofProxy(this); } @@ -353,6 +356,7 @@ ClauseId SatProof::registerClause(::Minisat::CRef clause, bool isInput) { d_inputClauses.insert(newId); } } + Debug("proof:sat:detailed") <<"registerClause " << d_clauseId[clause] << " " <<isInput << "\n"; return d_clauseId[clause]; } @@ -367,6 +371,7 @@ ClauseId SatProof::registerUnitClause(::Minisat::Lit lit, bool isInput) { d_inputClauses.insert(newId); } } + Debug("proof:sat:detailed") <<"registerUnitClause " << d_unitId[toInt(lit)] << " " << isInput <<"\n"; return d_unitId[toInt(lit)]; } @@ -527,10 +532,25 @@ void SatProof::toStream(std::ostream& out) { Unimplemented("native proof printing not supported yet"); } +void SatProof::storeUnitConflict(::Minisat::Lit conflict_lit) { + Assert (!d_storedUnitConflict); + d_unitConflictId = registerUnitClause(conflict_lit); + d_storedUnitConflict = true; + Debug("proof:sat:detailed") <<"storeUnitConflict " << d_unitConflictId << "\n"; +} + void SatProof::finalizeProof(::Minisat::CRef conflict_ref) { Assert(d_resStack.size() == 0); - //ClauseId conflict_id = getClauseId(conflict_ref); - ClauseId conflict_id = registerClause(conflict_ref); //FIXME + Assert (conflict_ref != ::Minisat::CRef_Undef); + ClauseId conflict_id; + if (conflict_ref == ::Minisat::CRef_Lazy) { + Assert (d_storedUnitConflict); + conflict_id = d_unitConflictId; + } else { + Assert (!d_storedUnitConflict); + conflict_id = registerClause(conflict_ref); //FIXME + } + Debug("proof:sat") << "proof::finalizeProof Final Conflict "; print(conflict_id); @@ -573,6 +593,14 @@ void SatProof::markDeleted(CRef clause) { } } +/// store mapping from theory atoms to new variables +void SatProof::storeAtom(::Minisat::Lit literal, Expr atom) { + (d_atomToVar.find(atom) == d_atomToVar.end()); + d_atomToVar[atom] = literal; +} + + + /// LFSCSatProof class std::string LFSCSatProof::varName(::Minisat::Lit lit) { @@ -613,6 +641,7 @@ void LFSCSatProof::collectLemmas(ClauseId id) { d_seenLemmas.insert(id); } + Assert (d_resChains.find(id) != d_resChains.end()); ResChain* res = d_resChains[id]; ClauseId start = res->getStart(); collectLemmas(start); @@ -658,6 +687,14 @@ void LFSCSatProof::printResolution(ClauseId id) { void LFSCSatProof::printInputClause(ClauseId id) { + if (isUnit(id)) { + ::Minisat::Lit lit = getUnit(id); + d_clauseSS << "(% " << clauseName(id) << " (holds (clc "; + d_clauseSS << varName(lit) << "cln ))"; + d_paren << ")"; + return; + } + ostringstream os; CRef ref = getClauseRef(id); Assert (ref != CRef_Undef); @@ -692,6 +729,7 @@ void LFSCSatProof::printVariables() { void LFSCSatProof::flush(std::ostream& out) { + out << d_atomsSS.str(); out << "(check \n"; d_paren <<")"; out << d_varSS.str(); @@ -705,7 +743,7 @@ void LFSCSatProof::flush(std::ostream& out) { void LFSCSatProof::toStream(std::ostream& out) { Debug("proof:sat") << " LFSCSatProof::printProof \n"; - + // first collect lemmas to print in reverse order collectLemmas(d_emptyClauseId); for(IdSet::iterator it = d_seenLemmas.begin(); it!= d_seenLemmas.end(); ++it) { @@ -713,13 +751,22 @@ void LFSCSatProof::toStream(std::ostream& out) { printResolution(*it); } } + printAtoms(); // last resolution to be printed is the empty clause printResolution(d_emptyClauseId); - + printClauses(); printVariables(); flush(out); } +void LFSCSatProof::printAtoms() { + d_atomsSS << "; Mapping between boolean variables and theory atoms \n"; + for (AtomToVar::iterator it = d_atomToVar.begin(); it != d_atomToVar.end(); ++it) { + d_atomsSS << "; " << it->first << " => v" << var(it->second) << "\n"; + } +} + + } /* CVC4 namespace */ diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h index d497a4eba..fb8966400 100644 --- a/src/proof/sat_proof.h +++ b/src/proof/sat_proof.h @@ -26,6 +26,8 @@ #include <ext/hash_map> #include <ext/hash_set> #include <sstream> +#include "expr/expr.h" + namespace Minisat { class Solver; @@ -90,6 +92,8 @@ typedef std::vector < ResChain* > ResStack; typedef std::hash_set < int > VarSet; typedef std::set < ClauseId > IdSet; typedef std::vector < ::Minisat::Lit > LitVector; +typedef __gnu_cxx::hash_map<Expr, ::Minisat::Lit, ExprHashFunction > AtomToVar; + class SatProof; class ProofProxy : public ProofProxyAbstract { @@ -124,7 +128,14 @@ protected: // temporary map for updating CRefs ClauseIdMap d_temp_clauseId; - IdClauseMap d_temp_idClause; + IdClauseMap d_temp_idClause; + + // unit conflict + ClauseId d_unitConflictId; + bool d_storedUnitConflict; + + // atom mapping + AtomToVar d_atomToVar; public: SatProof(::Minisat::Solver* solver, bool checkRes = false); protected: @@ -197,6 +208,9 @@ public: /// clause registration methods ClauseId registerClause(const ::Minisat::CRef clause, bool isInput = false); ClauseId registerUnitClause(const ::Minisat::Lit lit, bool isInput = false); + + void storeUnitConflict(::Minisat::Lit lit); + /** * Marks the deleted clauses as deleted. Note we may still use them in the final * resolution. @@ -216,12 +230,20 @@ public: */ void storeUnitResolution(::Minisat::Lit lit); - ProofProxy* getProxy() {return d_proxy; } + ProofProxy* getProxy() {return d_proxy; } + /** + * At mapping between literal and theory-atom it represents + * + * @param literal + * @param atom + */ + void storeAtom(::Minisat::Lit literal, Expr atom); };/* class SatProof */ class LFSCSatProof: public SatProof { private: - VarSet d_seenVars; + VarSet d_seenVars; + std::ostringstream d_atomsSS; std::ostringstream d_varSS; std::ostringstream d_lemmaSS; std::ostringstream d_clauseSS; @@ -239,11 +261,12 @@ private: void printVariables(); void printClauses(); void flush(std::ostream& out); - + void printAtoms(); public: LFSCSatProof(::Minisat::Solver* solver, bool checkRes = false): SatProof(solver, checkRes), d_seenVars(), + d_atomsSS(), d_varSS(), d_lemmaSS(), d_paren(), diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 4be58bdef..8ebb461e5 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -27,7 +27,9 @@ #include "expr/expr.h" #include "prop/theory_proxy.h" #include "theory/bv/options.h" - +#include "proof/proof_manager.h" +#include "proof/sat_proof.h" +#include "prop/minisat/minisat.h" #include <queue> using namespace std; @@ -236,7 +238,7 @@ SatLiteral CnfStream::convertAtom(TNode node) { // Make a new literal (variables are not considered theory literals) SatLiteral lit = newLiteral(node, theoryLiteral, preRegister, canEliminate); - + PROOF (ProofManager::getSatProof()->storeAtom(MinisatSatSolver::toMinisatLit(lit), node.toExpr()); ); // Return the resulting literal return lit; } diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 6196ca357..4cce83fef 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -261,6 +261,7 @@ CRef Solver::reason(Var x) { // Construct the reason CRef real_reason = ca.alloc(explLevel, explanation, true); + PROOF (ProofManager::getSatProof()->registerClause(real_reason, true); ); vardata[x] = VarData(real_reason, level(x), user_level(x), intro_level(x), trail_index(x)); clauses_removable.push(real_reason); attachClause(real_reason); @@ -298,7 +299,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable) continue; } // If a literals is false at 0 level (both sat and user level) we also ignore it - if (value(ps[i]) == l_False) { + if (value(ps[i]) == l_False && !PROOF_ON() ) { if (level(var(ps[i])) == 0 && user_level(var(ps[i])) == 0) { continue; } else { @@ -789,7 +790,8 @@ CRef Solver::propagate(TheoryCheckType type) // If there are lemmas (or conflicts) update them if (lemmas.size() > 0) { recheck = true; - return updateLemmas(); + confl = updateLemmas(); + return confl; } else { recheck = proxy->theoryNeedCheck(); return confl; @@ -801,7 +803,6 @@ CRef Solver::propagate(TheoryCheckType type) do { // Propagate on the clauses confl = propagateBool(); - // If no conflict, do the theory check if (confl == CRef_Undef && type != CHECK_WITHOUTH_THEORY) { // Do the theory check @@ -836,7 +837,6 @@ CRef Solver::propagate(TheoryCheckType type) } } } while (confl == CRef_Undef && qhead < trail.size()); - return confl; } @@ -1579,6 +1579,7 @@ CRef Solver::updateLemmas() { vec<Lit>& lemma = lemmas[i]; // If it's an empty lemma, we have a conflict at zero level if (lemma.size() == 0) { + Assert (! PROOF_ON()); conflict = CRef_Lazy; backtrackLevel = 0; Debug("minisat::lemmas") << "Solver::updateLemmas(): found empty clause" << std::endl; @@ -1628,6 +1629,7 @@ CRef Solver::updateLemmas() { } lemma_ref = ca.alloc(clauseLevel, lemma, removable); + PROOF (ProofManager::getSatProof()->registerClause(lemma_ref, true); ); if (removable) { clauses_removable.push(lemma_ref); } else { @@ -1647,6 +1649,7 @@ CRef Solver::updateLemmas() { } else { Debug("minisat::lemmas") << "Solver::updateLemmas(): unit conflict or empty clause" << std::endl; conflict = CRef_Lazy; + PROOF(ProofManager::getSatProof()->storeUnitConflict(lemma[0]);); } } else { Debug("minisat::lemmas") << "lemma size is " << lemma.size() << std::endl; diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 5d6356a5b..a169d31e6 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -83,7 +83,8 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext userContext, // fullLitToNode Map = options::threads() > 1 || - options::decisionMode() == decision::DECISION_STRATEGY_RELEVANCY); + options::decisionMode() == decision::DECISION_STRATEGY_RELEVANCY + ); d_satSolver->initialize(d_context, new TheoryProxy(this, d_theoryEngine, d_decisionEngine, d_context, d_cnfStream)); diff --git a/src/smt/options b/src/smt/options index 2680f4105..e5f9c2eaf 100644 --- a/src/smt/options +++ b/src/smt/options @@ -24,6 +24,8 @@ common-option produceModels produce-models -m --produce-models bool :default fal support the get-value and get-model commands option checkModels check-models --check-models bool :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions +option dumpModels --dump-models bool :default false + output models after every SAT/INVALID/UNKNOWN response option proof produce-proofs --proof bool :default false :predicate CVC4::smt::proofEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" turn on proof generation # this is just a placeholder for later; it doesn't show up in command-line options listings diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 76d4c973f..ca89ce36d 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -74,6 +74,7 @@ #include "util/sort_inference.h" #include "theory/quantifiers/macros.h" #include "theory/datatypes/options.h" +#include "theory/quantifiers/first_order_reasoning.h" using namespace std; using namespace CVC4; @@ -349,8 +350,8 @@ private: bool checkForBadSkolems(TNode n, TNode skolem, hash_map<Node, bool, NodeHashFunction>& cache); // Lift bit-vectors of size 1 to booleans - void bvToBool(); - + void bvToBool(); + // Simplify ITE structure void simpITE(); @@ -1009,11 +1010,18 @@ void SmtEngine::setLogicInternal() throw() { //for finite model finding if( ! options::instWhenMode.wasSetByUser()){ + //instantiate only on last call if( options::fmfInstEngine() ){ Trace("smt") << "setting inst when mode to LAST_CALL" << endl; options::instWhenMode.set( INST_WHEN_LAST_CALL ); } } + if ( ! options::fmfInstGen.wasSetByUser()) { + //if full model checking is on, disable inst-gen techniques + if( options::fmfFullModelCheck() ){ + options::fmfInstGen.set( false ); + } + } //until bugs 371,431 are fixed if( ! options::minisatUseElim.wasSetByUser()){ @@ -1824,15 +1832,15 @@ bool SmtEnginePrivate::nonClausalSimplify() { } hash_set<TNode, TNodeHashFunction> s; - Trace("debugging") << "NonClausal simplify pre-preprocess\n"; + Trace("debugging") << "NonClausal simplify pre-preprocess\n"; for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) { Node assertion = d_assertionsToPreprocess[i]; Node assertionNew = d_topLevelSubstitutions.apply(assertion); Trace("debugging") << "assertion = " << assertion << endl; - Trace("debugging") << "assertionNew = " << assertionNew << endl; + Trace("debugging") << "assertionNew = " << assertionNew << endl; if (assertion != assertionNew) { assertion = Rewriter::rewrite(assertionNew); - Trace("debugging") << "rewrite(assertion) = " << assertion << endl; + Trace("debugging") << "rewrite(assertion) = " << assertion << endl; } Assert(Rewriter::rewrite(assertion) == assertion); for (;;) { @@ -1841,11 +1849,11 @@ bool SmtEnginePrivate::nonClausalSimplify() { break; } ++d_smt.d_stats->d_numConstantProps; - Trace("debugging") << "assertionNew = " << assertionNew << endl; + Trace("debugging") << "assertionNew = " << assertionNew << endl; assertion = Rewriter::rewrite(assertionNew); - Trace("debugging") << "assertionNew = " << assertionNew << endl; + Trace("debugging") << "assertionNew = " << assertionNew << endl; } - Trace("debugging") << "\n"; + Trace("debugging") << "\n"; s.insert(assertion); d_assertionsToCheck.push_back(assertion); Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " @@ -1936,7 +1944,7 @@ bool SmtEnginePrivate::nonClausalSimplify() { void SmtEnginePrivate::bvToBool() { Trace("bv-to-bool") << "SmtEnginePrivate::bvToBool()" << endl; std::vector<Node> new_assertions; - d_smt.d_theoryEngine->ppBvToBool(d_assertionsToCheck, new_assertions); + d_smt.d_theoryEngine->ppBvToBool(d_assertionsToCheck, new_assertions); for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) { d_assertionsToCheck[i] = Rewriter::rewrite(new_assertions[i]); } @@ -2790,6 +2798,12 @@ void SmtEnginePrivate::processAssertions() { }while( success ); } + Trace("fo-rsn-enable") << std::endl; + if( options::foPropQuant() ){ + FirstOrderPropagation fop; + fop.simplify( d_assertionsToPreprocess ); + } + if( options::sortInference() ){ //sort inference technique d_smt.d_theoryEngine->getSortInference()->simplify( d_assertionsToPreprocess ); @@ -2810,7 +2824,7 @@ void SmtEnginePrivate::processAssertions() { } dumpAssertions("post-static-learning", d_assertionsToCheck); - // Lift bit-vectors of size 1 to bool + // Lift bit-vectors of size 1 to bool if(options::bvToBool()) { Chat() << "...doing bvToBool..." << endl; bvToBool(); @@ -2820,7 +2834,7 @@ void SmtEnginePrivate::processAssertions() { Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; - + dumpAssertions("pre-ite-removal", d_assertionsToCheck); { Chat() << "removing term ITEs..." << endl; diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp index 8454ca210..1ebbe49e0 100644 --- a/src/theory/arith/normal_form.cpp +++ b/src/theory/arith/normal_form.cpp @@ -745,9 +745,8 @@ bool Comparison::isNormalGEQ() const { return false; }else{ if(left.isIntegral()){ - return left.denominatorLCMIsOne() && left.numeratorGCDIsOne(); + return left.signNormalizedReducedSum(); }else{ - Debug("nf::tmp") << "imme sdfhkdjfh "<< left.leadingCoefficientIsAbsOne() << endl; return left.leadingCoefficientIsAbsOne(); } } @@ -768,7 +767,7 @@ bool Comparison::isNormalLT() const { return false; }else{ if(left.isIntegral()){ - return left.denominatorLCMIsOne() && left.numeratorGCDIsOne(); + return left.signNormalizedReducedSum(); }else{ return left.leadingCoefficientIsAbsOne(); } @@ -889,6 +888,7 @@ Node Comparison::mkIntInequality(Kind k, const Polynomial& p){ Polynomial left = sp.getPolynomial(); Rational right = - (sp.getConstant().getValue()); + Monomial m = left.getHead(); Assert(!m.isConstant()); @@ -899,16 +899,31 @@ Node Comparison::mkIntInequality(Kind k, const Polynomial& p){ Polynomial newLeft = left * mult; Rational rightMult = right * mult; + bool negateResult = false; + if(!newLeft.leadingCoefficientIsPositive()){ + // multiply by -1 + // a: left >= right or b: left > right + // becomes + // a: -left <= -right or b: -left < -right + // a: not (-left > -right) or b: (not -left >= -right) + newLeft = -newLeft; + rightMult = -rightMult; + k = (kind::GT == k) ? kind::GEQ : kind::GT; + negateResult = true; + // the later stages handle: + // a: not (-left >= -right + 1) or b: (not -left >= -right) + } + Node result = Node::null(); if(rightMult.isIntegral()){ if(k == kind::GT){ // (> p z) // (>= p (+ z 1)) Constant rightMultPlusOne = Constant::mkConstant(rightMult + 1); - return toNode(kind::GEQ, newLeft, rightMultPlusOne); + result = toNode(kind::GEQ, newLeft, rightMultPlusOne); }else{ Constant newRight = Constant::mkConstant(rightMult); - return toNode(kind::GEQ, newLeft, newRight); + result = toNode(kind::GEQ, newLeft, newRight); } }else{ //(>= l (/ n d)) @@ -916,7 +931,13 @@ Node Comparison::mkIntInequality(Kind k, const Polynomial& p){ //This also hold for GT as (ceil (/ n d)) > (/ n d) Integer ceilr = rightMult.ceiling(); Constant ceilRight = Constant::mkConstant(ceilr); - return toNode(kind::GEQ, newLeft, ceilRight); + result = toNode(kind::GEQ, newLeft, ceilRight); + } + Assert(!result.isNull()); + if(negateResult){ + return result.notNode(); + }else{ + return result; } } diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h index bcf9cbfa4..c6af7010f 100644 --- a/src/theory/arith/normal_form.h +++ b/src/theory/arith/normal_form.h @@ -76,12 +76,13 @@ namespace arith { * (exists realMonomial (monomialList qpolynomial)) * abs(monomialCoefficient (head (monomialList qpolynomial))) == 1 * - * integer_cmp := (<= zpolynomial constant) + * integer_cmp := (>= zpolynomial constant) * where * not (exists constantMonomial (monomialList zpolynomial)) * (forall integerMonomial (monomialList zpolynomial)) * the gcd of all numerators of coefficients is 1 * the denominator of all coefficients and the constant is 1 + * the leading coefficient is positive * * rational_eq := (= qvarlist qpolynomial) * where @@ -939,6 +940,10 @@ public: bool denominatorLCMIsOne() const; bool numeratorGCDIsOne() const; + bool signNormalizedReducedSum() const { + return leadingCoefficientIsPositive() && denominatorLCMIsOne() && numeratorGCDIsOne(); + } + /** * Returns the Least Common Multiple of the denominators of the coefficients * of the monomials. @@ -1265,7 +1270,7 @@ private: * Creates a comparison equivalent to (k l 0). * k is either GT or GEQ. * It is not the case that all variables in l are integral. - */ + */ static Node mkRatInequality(Kind k, const Polynomial& l); public: diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index d911ecf77..060f6dbba 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -67,6 +67,8 @@ #include "theory/arith/options.h" +#include "theory/quantifiers/bounded_integers.h" + #include <stdint.h> #include <vector> @@ -89,6 +91,7 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, context::Context d_unknownsInARow(0), d_hasDoneWorkSinceCut(false), d_learner(u), + d_quantEngine(qe), d_assertionsThatDoNotMatchTheirLiterals(c), d_nextIntegerCheckVar(0), d_constantIntegerVariables(c), @@ -1373,6 +1376,10 @@ Constraint TheoryArithPrivate::constraintFromFactQueue(){ Assert(!done()); TNode assertion = get(); + if( options::finiteModelFind() ){ + d_quantEngine->getBoundedIntegers()->assertNode(assertion); + } + Kind simpleKind = Comparison::comparisonKind(assertion); Constraint constraint = d_constraintDatabase.lookup(assertion); if(constraint == NullConstraint){ diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 2ea3bb68e..86c8e213e 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -132,7 +132,8 @@ private: /** Static learner. */ ArithStaticLearner d_learner; - + /** quantifiers engine */ + QuantifiersEngine * d_quantEngine; //std::vector<ArithVar> d_pool; public: void releaseArithVar(ArithVar v); diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h index 8374a3f75..1c6920236 100644 --- a/src/theory/bv/bv_subtheory.h +++ b/src/theory/bv/bv_subtheory.h @@ -55,9 +55,6 @@ inline std::ostream& operator << (std::ostream& out, SubTheory subtheory) { } -const bool d_useEqualityEngine = true; -const bool d_useSatPropagation = true; - // forward declaration class TheoryBV; diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp index 2308f36a3..244d87233 100644 --- a/src/theory/bv/bv_subtheory_bitblast.cpp +++ b/src/theory/bv/bv_subtheory_bitblast.cpp @@ -34,7 +34,8 @@ BitblastSolver::BitblastSolver(context::Context* c, TheoryBV* bv) d_bitblaster(new Bitblaster(c, bv)), d_bitblastQueue(c), d_statistics(), - d_validModelCache(c, true) + d_validModelCache(c, true), + d_useSatPropagation(options::bvPropagate()) {} BitblastSolver::~BitblastSolver() { diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h index 819b3d62c..315254c8e 100644 --- a/src/theory/bv/bv_subtheory_bitblast.h +++ b/src/theory/bv/bv_subtheory_bitblast.h @@ -47,6 +47,7 @@ class BitblastSolver : public SubtheorySolver { context::CDO<bool> d_validModelCache; Node getModelValueRec(TNode node); + bool d_useSatPropagation; 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 c0546f892..f7209d326 100644 --- a/src/theory/bv/bv_subtheory_core.cpp +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -37,40 +37,38 @@ CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv) d_isCoreTheory(c, true), d_reasons(c) { - if (d_useEqualityEngine) { - // The kinds we are treating as function application in congruence - d_equalityEngine.addFunctionKind(kind::BITVECTOR_CONCAT, true); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_AND); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_OR); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_XOR); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOT); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NAND); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOR); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_XNOR); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_COMP); - d_equalityEngine.addFunctionKind(kind::BITVECTOR_MULT, true); - d_equalityEngine.addFunctionKind(kind::BITVECTOR_PLUS, true); - d_equalityEngine.addFunctionKind(kind::BITVECTOR_EXTRACT, true); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SUB); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NEG); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UDIV); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UREM); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SDIV); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SREM); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SMOD); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SHL); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_LSHR); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ASHR); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULT); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULE); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGT); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGE); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLT); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLE); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGT); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGE); - } + // The kinds we are treating as function application in congruence + d_equalityEngine.addFunctionKind(kind::BITVECTOR_CONCAT, true); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_AND); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_OR); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_XOR); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOT); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NAND); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOR); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_XNOR); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_COMP); + d_equalityEngine.addFunctionKind(kind::BITVECTOR_MULT, true); + d_equalityEngine.addFunctionKind(kind::BITVECTOR_PLUS, true); + d_equalityEngine.addFunctionKind(kind::BITVECTOR_EXTRACT, true); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SUB); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NEG); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UDIV); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UREM); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SDIV); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SREM); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SMOD); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SHL); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_LSHR); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ASHR); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULT); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULE); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGT); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGE); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLT); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLE); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGT); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGE); } CoreSolver::~CoreSolver() { @@ -81,9 +79,6 @@ void CoreSolver::setMasterEqualityEngine(eq::EqualityEngine* eq) { } void CoreSolver::preRegister(TNode node) { - if (!d_useEqualityEngine) - return; - if (node.getKind() == kind::EQUAL) { d_equalityEngine.addTriggerEquality(node); if (options::bitvectorCoreSolver()) { @@ -291,7 +286,7 @@ void CoreSolver::buildModel() { bool CoreSolver::assertFactToEqualityEngine(TNode fact, TNode reason) { // Notify the equality engine - if (d_useEqualityEngine && !d_bv->inConflict() && (!d_bv->wasPropagatedBySubtheory(fact) || !d_bv->getPropagatingSubtheory(fact) == SUB_CORE)) { + if (!d_bv->inConflict() && (!d_bv->wasPropagatedBySubtheory(fact) || !d_bv->getPropagatingSubtheory(fact) == SUB_CORE)) { Debug("bv-slicer-eq") << "CoreSolver::assertFactToEqualityEngine fact=" << fact << endl; // Debug("bv-slicer-eq") << " reason=" << reason << endl; bool negated = fact.getKind() == kind::NOT; diff --git a/src/theory/bv/options b/src/theory/bv/options index 7b87baa21..077299d1f 100644 --- a/src/theory/bv/options +++ b/src/theory/bv/options @@ -22,5 +22,11 @@ option bitvectorCoreSolver --bv-core-solver bool option bvToBool --bv-to-bool bool lift bit-vectors of size 1 to booleans when possible + +option bvPropagate --bv-propagate bool :default true + use bit-vector propagation in the bit-blaster + +option bvEquality --bv-eq bool :default true + use the equality engine for the bit-vector theory endmodule diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 4803fd62e..224359952 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -49,10 +49,11 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& d_literalsToPropagateIndex(c, 0), d_propagatedBy(c) { - SubtheorySolver* core_solver = new CoreSolver(c, this); - d_subtheories.push_back(core_solver); - d_subtheoryMap[SUB_CORE] = core_solver; - + if (options::bvEquality()) { + SubtheorySolver* core_solver = new CoreSolver(c, this); + d_subtheories.push_back(core_solver); + d_subtheoryMap[SUB_CORE] = core_solver; + } if (options::bitvectorInequalitySolver()) { SubtheorySolver* ineq_solver = new InequalitySolver(c, this); d_subtheories.push_back(ineq_solver); @@ -366,7 +367,7 @@ Node TheoryBV::explain(TNode node) { void TheoryBV::addSharedTerm(TNode t) { Debug("bitvector::sharing") << indent() << "TheoryBV::addSharedTerm(" << t << ")" << std::endl; d_sharedTermsSet.insert(t); - if (!options::bitvectorEagerBitblast() && d_useEqualityEngine) { + if (!options::bitvectorEagerBitblast() && options::bvEquality()) { for (unsigned i = 0; i < d_subtheories.size(); ++i) { d_subtheories[i]->addSharedTerm(t); } diff --git a/src/theory/quantifiers/Makefile.am b/src/theory/quantifiers/Makefile.am index 7fea8cf3a..92d780be4 100644 --- a/src/theory/quantifiers/Makefile.am +++ b/src/theory/quantifiers/Makefile.am @@ -44,7 +44,13 @@ libquantifiers_la_SOURCES = \ inst_strategy_e_matching.h \ inst_strategy_e_matching.cpp \ inst_strategy_cbqi.h \ - inst_strategy_cbqi.cpp + inst_strategy_cbqi.cpp \ + full_model_check.h \ + full_model_check.cpp \ + bounded_integers.h \ + bounded_integers.cpp \ + first_order_reasoning.h \ + first_order_reasoning.cpp EXTRA_DIST = \ kinds \ diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp new file mode 100755 index 000000000..aeac3c79b --- /dev/null +++ b/src/theory/quantifiers/bounded_integers.cpp @@ -0,0 +1,291 @@ +/********************* */
+/*! \file bounded_integers.cpp
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Bounded integers module
+ **
+ ** This class manages integer bounds for quantifiers
+ **/
+
+#include "theory/quantifiers/bounded_integers.h"
+#include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/first_order_model.h"
+
+using namespace CVC4;
+using namespace std;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+using namespace CVC4::kind;
+
+void BoundedIntegers::RangeModel::initialize() {
+ //add initial split lemma
+ Node ltr = NodeManager::currentNM()->mkNode( LT, d_range, NodeManager::currentNM()->mkConst( Rational(0) ) );
+ ltr = Rewriter::rewrite( ltr );
+ Trace("bound-integers-lemma") << " *** bound int: initial split on " << ltr << std::endl;
+ d_bi->getQuantifiersEngine()->getOutputChannel().split( ltr );
+ Node ltr_lit = ltr.getKind()==NOT ? ltr[0] : ltr;
+ d_range_literal[-1] = ltr_lit;
+ d_lit_to_range[ltr_lit] = -1;
+ d_lit_to_pol[ltr_lit] = ltr.getKind()!=NOT;
+ //register with bounded integers
+ Trace("bound-integers-debug") << "Literal " << ltr_lit << " is literal for " << d_range << std::endl;
+ d_bi->addLiteralFromRange(ltr_lit, d_range);
+}
+
+void BoundedIntegers::RangeModel::assertNode(Node n) {
+ bool pol = n.getKind()!=NOT;
+ Node nlit = n.getKind()==NOT ? n[0] : n;
+ if( d_lit_to_range.find( nlit )!=d_lit_to_range.end() ){
+ Trace("bound-integers-assert") << "With polarity = " << pol << " (req "<< d_lit_to_pol[nlit] << ")";
+ Trace("bound-integers-assert") << ", found literal " << nlit;
+ Trace("bound-integers-assert") << ", it is bound literal " << d_lit_to_range[nlit] << " for " << d_range << std::endl;
+ d_range_assertions[nlit] = (pol==d_lit_to_pol[nlit]);
+ if( pol!=d_lit_to_pol[nlit] ){
+ //check if we need a new split?
+ if( !d_has_range ){
+ bool needsRange = true;
+ for( std::map< Node, int >::iterator it = d_lit_to_range.begin(); it != d_lit_to_range.end(); ++it ){
+ if( d_range_assertions.find( it->first )==d_range_assertions.end() ){
+ needsRange = false;
+ break;
+ }
+ }
+ if( needsRange ){
+ allocateRange();
+ }
+ }
+ }else{
+ if (!d_has_range || d_lit_to_range[nlit]<d_curr_range ){
+ Trace("bound-integers-bound") << "Successfully bound " << d_range << " to " << d_lit_to_range[nlit] << std::endl;
+ d_curr_range = d_lit_to_range[nlit];
+ }
+ //set the range
+ d_has_range = true;
+ }
+ }else{
+ Message() << "Could not find literal " << nlit << " for range " << d_range << std::endl;
+ exit(0);
+ }
+}
+
+void BoundedIntegers::RangeModel::allocateRange() {
+ d_curr_max++;
+ int newBound = d_curr_max;
+ Trace("bound-integers-proc") << "Allocate range bound " << newBound << " for " << d_range << std::endl;
+ //TODO: newBound should be chosen in a smarter way
+ Node ltr = NodeManager::currentNM()->mkNode( LEQ, d_range, NodeManager::currentNM()->mkConst( Rational(newBound) ) );
+ ltr = Rewriter::rewrite( ltr );
+ Trace("bound-integers-lemma") << " *** bound int: split on " << ltr << std::endl;
+ d_bi->getQuantifiersEngine()->getOutputChannel().split( ltr );
+ Node ltr_lit = ltr.getKind()==NOT ? ltr[0] : ltr;
+ d_range_literal[newBound] = ltr_lit;
+ d_lit_to_range[ltr_lit] = newBound;
+ d_lit_to_pol[ltr_lit] = ltr.getKind()!=NOT;
+ //register with bounded integers
+ d_bi->addLiteralFromRange(ltr_lit, d_range);
+}
+
+Node BoundedIntegers::RangeModel::getNextDecisionRequest() {
+ //request the current cardinality as a decision literal, if not already asserted
+ for( std::map< Node, int >::iterator it = d_lit_to_range.begin(); it != d_lit_to_range.end(); ++it ){
+ int i = it->second;
+ if( !d_has_range || i<d_curr_range ){
+ Node rn = it->first;
+ Assert( !rn.isNull() );
+ if( d_range_assertions.find( rn )==d_range_assertions.end() ){
+ if (!d_lit_to_pol[it->first]) {
+ rn = rn.negate();
+ }
+ Trace("bound-integers-dec") << "For " << d_range << ", make decision " << rn << " to make range " << i << std::endl;
+ return rn;
+ }
+ }
+ }
+ return Node::null();
+}
+
+
+BoundedIntegers::BoundedIntegers(context::Context* c, QuantifiersEngine* qe) :
+QuantifiersModule(qe), d_assertions(c){
+
+}
+
+bool BoundedIntegers::isBound( Node f, Node v ) {
+ return std::find( d_set[f].begin(), d_set[f].end(), v )!=d_set[f].end();
+}
+
+bool BoundedIntegers::hasNonBoundVar( Node f, Node b ) {
+ if( b.getKind()==BOUND_VARIABLE ){
+ if( isBound( f, b ) ){
+ return true;
+ }
+ }else{
+ for( unsigned i=0; i<b.getNumChildren(); i++ ){
+ if( hasNonBoundVar( f, b[i] ) ){
+ return true;
+ }
+ }
+ }
+ return false;
+}
+
+void BoundedIntegers::processLiteral( Node f, Node lit, bool pol ) {
+ if( lit.getKind()==GEQ && lit[0].getType().isInteger() ){
+ std::map< Node, Node > msum;
+ if (QuantArith::getMonomialSumLit( lit, msum )){
+ Trace("bound-integers-debug") << "Literal (polarity = " << pol << ") " << lit << " is monomial sum : " << std::endl;
+ for(std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
+ Trace("bound-integers-debug") << " ";
+ if( !it->second.isNull() ){
+ Trace("bound-integers-debug") << it->second;
+ if( !it->first.isNull() ){
+ Trace("bound-integers-debug") << " * ";
+ }
+ }
+ if( !it->first.isNull() ){
+ Trace("bound-integers-debug") << it->first;
+ }
+ Trace("bound-integers-debug") << std::endl;
+ }
+ Trace("bound-integers-debug") << std::endl;
+ for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
+ if ( !it->first.isNull() && it->first.getKind()==BOUND_VARIABLE ){
+ Node veq;
+ if( QuantArith::isolate( it->first, msum, veq, GEQ ) ){
+ Node n1 = veq[0];
+ Node n2 = veq[1];
+ if(pol){
+ //flip
+ n1 = veq[1];
+ n2 = veq[0];
+ if( n1.getKind()==BOUND_VARIABLE ){
+ n2 = QuantArith::offset( n2, 1 );
+ }else{
+ n1 = QuantArith::offset( n1, -1 );
+ }
+ veq = NodeManager::currentNM()->mkNode( GEQ, n1, n2 );
+ }
+ Trace("bound-integers-debug") << "Isolated for " << it->first << " : (" << n1 << " >= " << n2 << ")" << std::endl;
+ Node bv = n1.getKind()==BOUND_VARIABLE ? n1 : n2;
+ if( !isBound( f, bv ) ){
+ if( !hasNonBoundVar( f, n1.getKind()==BOUND_VARIABLE ? n2 : n1 ) ) {
+ Trace("bound-integers-debug") << "The bound is relevant." << std::endl;
+ d_bounds[n1.getKind()==BOUND_VARIABLE ? 0 : 1][f][bv] = (n1.getKind()==BOUND_VARIABLE ? n2 : n1);
+ }
+ }
+ }
+ }
+ }
+ }
+ }else if( lit.getKind()==LEQ || lit.getKind()==LT || lit.getKind()==GT ) {
+ std::cout << "BoundedIntegers : Bad kind for literal : " << lit << std::endl;
+ exit(0);
+ }
+}
+
+void BoundedIntegers::process( Node f, Node n, bool pol ){
+ if( (( n.getKind()==IMPLIES || n.getKind()==OR) && pol) || (n.getKind()==AND && !pol) ){
+ for( unsigned i=0; i<n.getNumChildren(); i++) {
+ bool newPol = n.getKind()==IMPLIES && i==0 ? !pol : pol;
+ process( f, n[i], newPol );
+ }
+ }else if( n.getKind()==NOT ){
+ process( f, n[0], !pol );
+ }else {
+ processLiteral( f, n, pol );
+ }
+}
+
+void BoundedIntegers::check( Theory::Effort e ) {
+
+}
+
+
+void BoundedIntegers::addLiteralFromRange( Node lit, Node r ) {
+ d_lit_to_ranges[lit].push_back(r);
+ //check if it is already asserted?
+ if(d_assertions.find(lit)!=d_assertions.end()){
+ d_rms[r]->assertNode( d_assertions[lit] ? lit : lit.negate() );
+ }
+}
+
+void BoundedIntegers::registerQuantifier( Node f ) {
+ Trace("bound-integers") << "Register quantifier " << f << std::endl;
+ bool hasIntType = false;
+ for( unsigned i=0; i<f[0].getNumChildren(); i++) {
+ if( f[0][i].getType().isInteger() ){
+ hasIntType = true;
+ break;
+ }
+ }
+ if( hasIntType ){
+ bool success;
+ do{
+ success = false;
+ process( f, f[1], true );
+ for( std::map< Node, Node >::iterator it = d_bounds[0][f].begin(); it != d_bounds[0][f].end(); ++it ){
+ Node v = it->first;
+ if( !isBound(f,v) ){
+ if( d_bounds[1][f].find(v)!=d_bounds[1][f].end() ){
+ d_set[f].push_back(v);
+ success = true;
+ }
+ }
+ }
+ }while( success );
+ Trace("bound-integers") << "Bounds are : " << std::endl;
+ for( unsigned i=0; i<d_set[f].size(); i++) {
+ Node v = d_set[f][i];
+ Node r = NodeManager::currentNM()->mkNode( MINUS, d_bounds[1][f][v], d_bounds[0][f][v] );
+ d_range[f][v] = Rewriter::rewrite( r );
+ Trace("bound-integers") << " " << d_bounds[0][f][v] << " <= " << v << " <= " << d_bounds[1][f][v] << " (range is " << d_range[f][v] << ")" << std::endl;
+ }
+ if( d_set[f].size()==f[0].getNumChildren() ){
+ d_bound_quants.push_back( f );
+ for( unsigned i=0; i<d_set[f].size(); i++) {
+ Node v = d_set[f][i];
+ Node r = d_range[f][v];
+ if( std::find(d_ranges.begin(), d_ranges.end(), r)==d_ranges.end() ){
+ d_ranges.push_back( r );
+ d_rms[r] = new RangeModel(this, r, d_quantEngine->getSatContext() );
+ d_rms[r]->initialize();
+ }
+ }
+ }
+ }
+}
+
+void BoundedIntegers::assertNode( Node n ) {
+ Trace("bound-integers-assert") << "Assert " << n << std::endl;
+ Node nlit = n.getKind()==NOT ? n[0] : n;
+ if( d_lit_to_ranges.find(nlit)!=d_lit_to_ranges.end() ){
+ Trace("bound-integers-assert") << "This is the bounding literal for " << d_lit_to_ranges[nlit].size() << " ranges." << std::endl;
+ for( unsigned i=0; i<d_lit_to_ranges[nlit].size(); i++) {
+ Node r = d_lit_to_ranges[nlit][i];
+ Trace("bound-integers-assert") << " ...this is a bounding literal for " << r << std::endl;
+ d_rms[r]->assertNode( n );
+ }
+ }
+ d_assertions[nlit] = n.getKind()!=NOT;
+}
+
+Node BoundedIntegers::getNextDecisionRequest() {
+ Trace("bound-integers-dec") << "bi: Get next decision request?" << std::endl;
+ for( unsigned i=0; i<d_ranges.size(); i++) {
+ Node d = d_rms[d_ranges[i]]->getNextDecisionRequest();
+ if (!d.isNull()) {
+ return d;
+ }
+ }
+ return Node::null();
+}
+
+
+Node BoundedIntegers::getValueInModel( Node n ) {
+ return d_quantEngine->getModel()->getValue( n );
+}
\ No newline at end of file diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h new file mode 100755 index 000000000..4445493c9 --- /dev/null +++ b/src/theory/quantifiers/bounded_integers.h @@ -0,0 +1,94 @@ +/********************* */
+/*! \file bounded_integers.h
+** \verbatim
+** Original author: Andrew Reynolds
+** This file is part of the CVC4 project.
+** Copyright (c) 2009-2013 New York University and The University of Iowa
+** See the file COPYING in the top-level source directory for licensing
+** information.\endverbatim
+**
+** \brief This class manages integer bounds for quantifiers
+**/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__BOUNDED_INTEGERS_H
+#define __CVC4__BOUNDED_INTEGERS_H
+
+
+#include "theory/quantifiers_engine.h"
+
+#include "context/context.h"
+#include "context/context_mm.h"
+#include "context/cdchunk_list.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class BoundedIntegers : public QuantifiersModule
+{
+ typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
+ typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
+ typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
+private:
+ //for determining bounds
+ bool isBound( Node f, Node v );
+ bool hasNonBoundVar( Node f, Node b );
+ std::map< Node, std::map< Node, Node > > d_bounds[2];
+ std::map< Node, std::vector< Node > > d_set;
+ std::map< Node, std::map< Node, Node > > d_range;
+ void hasFreeVar( Node f, Node n );
+ void process( Node f, Node n, bool pol );
+ void processLiteral( Node f, Node lit, bool pol );
+ std::vector< Node > d_bound_quants;
+private:
+ class RangeModel {
+ private:
+ BoundedIntegers * d_bi;
+ void allocateRange();
+ public:
+ RangeModel(BoundedIntegers * bi, Node r, context::Context* c) : d_bi(bi),
+ d_range(r), d_curr_max(-1), d_range_assertions(c), d_has_range(c,false), d_curr_range(c,-1) {}
+ Node d_range;
+ int d_curr_max;
+ std::map< int, Node > d_range_literal;
+ std::map< Node, bool > d_lit_to_pol;
+ std::map< Node, int > d_lit_to_range;
+ NodeBoolMap d_range_assertions;
+ context::CDO< bool > d_has_range;
+ context::CDO< int > d_curr_range;
+ void initialize();
+ void assertNode(Node n);
+ Node getNextDecisionRequest();
+ };
+ Node getValueInModel( Node n );
+private:
+ //information for minimizing ranges
+ std::vector< Node > d_ranges;
+ //map to range model objects
+ std::map< Node, RangeModel * > d_rms;
+ //literal to range
+ std::map< Node, std::vector< Node > > d_lit_to_ranges;
+ //list of currently asserted arithmetic literals
+ NodeBoolMap d_assertions;
+private:
+ void addLiteralFromRange( Node lit, Node r );
+public:
+ BoundedIntegers( context::Context* c, QuantifiersEngine* qe );
+
+ void check( Theory::Effort e );
+ void registerQuantifier( Node f );
+ void assertNode( Node n );
+ Node getNextDecisionRequest();
+ Node getLowerBound( Node f, Node v ){ return d_bounds[0][f][v]; }
+ Node getUpperBound( Node f, Node v ){ return d_bounds[1][f][v]; }
+ Node getLowerBoundValue( Node f, Node v ){ return getValueInModel( d_bounds[0][f][v] ); }
+ Node getUpperBoundValue( Node f, Node v ){ return getValueInModel( d_bounds[1][f][v] ); }
+};
+
+}
+}
+}
+
+#endif
\ No newline at end of file diff --git a/src/theory/quantifiers/first_order_reasoning.cpp b/src/theory/quantifiers/first_order_reasoning.cpp new file mode 100755 index 000000000..27fcebccf --- /dev/null +++ b/src/theory/quantifiers/first_order_reasoning.cpp @@ -0,0 +1,171 @@ +/********************* */
+/*! \file first_order_reasoning.cpp
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief first order reasoning module
+ **
+ **/
+
+#include <vector>
+
+#include "theory/quantifiers/first_order_reasoning.h"
+#include "theory/rewriter.h"
+
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace std;
+
+namespace CVC4 {
+
+
+void FirstOrderPropagation::collectLits( Node n, std::vector<Node> & lits ){
+ if( n.getKind()==FORALL ){
+ collectLits( n[1], lits );
+ }else if( n.getKind()==OR ){
+ for(unsigned j=0; j<n.getNumChildren(); j++) {
+ collectLits(n[j], lits );
+ }
+ }else{
+ lits.push_back( n );
+ }
+}
+
+void FirstOrderPropagation::simplify( std::vector< Node >& assertions ){
+ for( unsigned i=0; i<assertions.size(); i++) {
+ Trace("fo-rsn") << "Assert : " << assertions[i] << std::endl;
+ }
+
+ //process all assertions
+ int num_processed;
+ int num_true = 0;
+ int num_rounds = 0;
+ do {
+ num_processed = 0;
+ for( unsigned i=0; i<assertions.size(); i++ ){
+ if( d_assertion_true.find(assertions[i])==d_assertion_true.end() ){
+ std::vector< Node > fo_lits;
+ collectLits( assertions[i], fo_lits );
+ Node unitLit = process( assertions[i], fo_lits );
+ if( !unitLit.isNull() ){
+ Trace("fo-rsn-debug") << "...possible unit literal : " << unitLit << " from " << assertions[i] << std::endl;
+ bool pol = unitLit.getKind()!=NOT;
+ unitLit = unitLit.getKind()==NOT ? unitLit[0] : unitLit;
+ if( unitLit.getKind()==EQUAL ){
+
+ }else if( unitLit.getKind()==APPLY_UF ){
+ //make sure all are unique vars;
+ bool success = true;
+ std::vector< Node > unique_vars;
+ for( unsigned j=0; j<unitLit.getNumChildren(); j++) {
+ if( unitLit[j].getKind()==BOUND_VARIABLE ){
+ if( std::find(unique_vars.begin(), unique_vars.end(), unitLit[j])==unique_vars.end() ){
+ unique_vars.push_back( unitLit[j] );
+ }else{
+ success = false;
+ break;
+ }
+ }else{
+ success = false;
+ break;
+ }
+ }
+ if( success ){
+ d_const_def[unitLit.getOperator()] = NodeManager::currentNM()->mkConst(pol);
+ Trace("fo-rsn") << "Propagate : " << unitLit.getOperator() << " == " << pol << std::endl;
+ Trace("fo-rsn") << " from : " << assertions[i] << std::endl;
+ d_assertion_true[assertions[i]] = true;
+ num_processed++;
+ }
+ }else if( unitLit.getKind()==VARIABLE ){
+ d_const_def[unitLit] = NodeManager::currentNM()->mkConst(pol);
+ Trace("fo-rsn") << "Propagate variable : " << unitLit << " == " << pol << std::endl;
+ Trace("fo-rsn") << " from : " << assertions[i] << std::endl;
+ d_assertion_true[assertions[i]] = true;
+ num_processed++;
+ }
+ }
+ if( d_assertion_true.find(assertions[i])!=d_assertion_true.end() ){
+ num_true++;
+ }
+ }
+ }
+ num_rounds++;
+ }while( num_processed>0 );
+ Trace("fo-rsn-sum") << "Simplified " << num_true << " / " << assertions.size() << " in " << num_rounds << " rounds." << std::endl;
+ for( unsigned i=0; i<assertions.size(); i++ ){
+ assertions[i] = theory::Rewriter::rewrite( simplify( assertions[i] ) );
+ }
+}
+
+Node FirstOrderPropagation::process(Node a, std::vector< Node > & lits) {
+ int index = -1;
+ for( unsigned i=0; i<lits.size(); i++) {
+ bool pol = lits[i].getKind()!=NOT;
+ Node n = lits[i].getKind()==NOT ? lits[i][0] : lits[i];
+ Node litDef;
+ if( n.getKind()==APPLY_UF ){
+ if( d_const_def.find(n.getOperator())!=d_const_def.end() ){
+ litDef = d_const_def[n.getOperator()];
+ }
+ }else if( n.getKind()==VARIABLE ){
+ if( d_const_def.find(n)!=d_const_def.end() ){
+ litDef = d_const_def[n];
+ }
+ }
+ if( !litDef.isNull() ){
+ Node poln = NodeManager::currentNM()->mkConst( pol );
+ if( litDef==poln ){
+ Trace("fo-rsn-debug") << "Assertion " << a << " is true because of " << lits[i] << std::endl;
+ d_assertion_true[a] = true;
+ return Node::null();
+ }
+ }
+ if( litDef.isNull() ){
+ if( index==-1 ){
+ //store undefined index
+ index = i;
+ }else{
+ //two undefined, return null
+ return Node::null();
+ }
+ }
+ }
+ if( index!=-1 ){
+ return lits[index];
+ }else{
+ return Node::null();
+ }
+}
+
+Node FirstOrderPropagation::simplify( Node n ) {
+ if( n.getKind()==VARIABLE ){
+ if( d_const_def.find(n)!=d_const_def.end() ){
+ return d_const_def[n];
+ }
+ }else if( n.getKind()==APPLY_UF ){
+ if( d_const_def.find(n.getOperator())!=d_const_def.end() ){
+ return d_const_def[n.getOperator()];
+ }
+ }
+ if( n.getNumChildren()==0 ){
+ return n;
+ }else{
+ std::vector< Node > children;
+ if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+ children.push_back( n.getOperator() );
+ }
+ for(unsigned i=0; i<n.getNumChildren(); i++) {
+ children.push_back( simplify(n[i]) );
+ }
+ return NodeManager::currentNM()->mkNode( n.getKind(), children );
+ }
+}
+
+}
diff --git a/src/theory/quantifiers/first_order_reasoning.h b/src/theory/quantifiers/first_order_reasoning.h new file mode 100755 index 000000000..0dbf23a3b --- /dev/null +++ b/src/theory/quantifiers/first_order_reasoning.h @@ -0,0 +1,45 @@ +/********************* */
+/*! \file first_order_reasoning.h
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Pre-process step for first-order reasoning
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__FIRST_ORDER_REASONING_H
+#define __CVC4__FIRST_ORDER_REASONING_H
+
+#include <iostream>
+#include <string>
+#include <vector>
+#include <map>
+#include "expr/node.h"
+#include "expr/type_node.h"
+
+namespace CVC4 {
+
+class FirstOrderPropagation {
+private:
+ std::map< Node, Node > d_const_def;
+ std::map< Node, bool > d_assertion_true;
+ Node process(Node a, std::vector< Node > & lits);
+ void collectLits( Node n, std::vector<Node> & lits );
+ Node simplify( Node n );
+public:
+ FirstOrderPropagation(){}
+ ~FirstOrderPropagation(){}
+
+ void simplify( std::vector< Node >& assertions );
+};
+
+}
+
+#endif
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp new file mode 100755 index 000000000..c2a3f895b --- /dev/null +++ b/src/theory/quantifiers/full_model_check.cpp @@ -0,0 +1,999 @@ +
+/********************* */
+/*! \file full_model_check.cpp
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Implementation of full model check class
+ **/
+
+#include "theory/quantifiers/full_model_check.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/options.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+using namespace CVC4::theory::inst;
+using namespace CVC4::theory::quantifiers::fmcheck;
+
+
+bool EntryTrie::hasGeneralization( FullModelChecker * m, Node c, int index ) {
+ if (index==(int)c.getNumChildren()) {
+ return d_data!=-1;
+ }else{
+ Node st = m->getStar(c[index].getType());
+ if(d_child.find(st)!=d_child.end()) {
+ if( d_child[st].hasGeneralization(m, c, index+1) ){
+ return true;
+ }
+ }
+ if( d_child.find( c[index] )!=d_child.end() ){
+ if( d_child[ c[index] ].hasGeneralization(m, c, index+1) ){
+ return true;
+ }
+ }
+ return false;
+ }
+}
+
+int EntryTrie::getGeneralizationIndex( FullModelChecker * m, std::vector<Node> & inst, int index ) {
+ if (index==(int)inst.size()) {
+ return d_data;
+ }else{
+ int minIndex = -1;
+ Node st = m->getStar(inst[index].getType());
+ if(d_child.find(st)!=d_child.end()) {
+ minIndex = d_child[st].getGeneralizationIndex(m, inst, index+1);
+ }
+ Node cc = inst[index];
+ if( d_child.find( cc )!=d_child.end() ){
+ int gindex = d_child[ cc ].getGeneralizationIndex(m, inst, index+1);
+ if (minIndex==-1 || (gindex!=-1 && gindex<minIndex) ){
+ minIndex = gindex;
+ }
+ }
+ return minIndex;
+ }
+}
+
+void EntryTrie::addEntry( FullModelChecker * m, Node c, Node v, int data, int index ) {
+ if (index==(int)c.getNumChildren()) {
+ if(d_data==-1) {
+ d_data = data;
+ }
+ }
+ else {
+ d_child[ c[index] ].addEntry(m,c,v,data,index+1);
+ }
+}
+
+void EntryTrie::getEntries( FullModelChecker * m, Node c, std::vector<int> & compat, std::vector<int> & gen, int index, bool is_gen ) {
+ if (index==(int)c.getNumChildren()) {
+ if( d_data!=-1) {
+ if( is_gen ){
+ gen.push_back(d_data);
+ }
+ compat.push_back(d_data);
+ }
+ }else{
+ if (m->isStar(c[index])) {
+ for ( std::map<Node,EntryTrie>::iterator it = d_child.begin(); it != d_child.end(); ++it ){
+ it->second.getEntries(m, c, compat, gen, index+1, is_gen );
+ }
+ }else{
+ Node st = m->getStar(c[index].getType());
+ if(d_child.find(st)!=d_child.end()) {
+ d_child[st].getEntries(m, c, compat, gen, index+1, false);
+ }
+ if( d_child.find( c[index] )!=d_child.end() ){
+ d_child[ c[index] ].getEntries(m, c, compat, gen, index+1, is_gen);
+ }
+ }
+
+ }
+}
+
+bool EntryTrie::getWitness( FullModelChecker * m, FirstOrderModel * fm, Node c, std::vector<Node> & inst, int index) {
+
+ return false;
+}
+
+
+bool Def::addEntry( FullModelChecker * m, Node c, Node v) {
+ if (!d_et.hasGeneralization(m, c)) {
+ int newIndex = (int)d_cond.size();
+ if (!d_has_simplified) {
+ std::vector<int> compat;
+ std::vector<int> gen;
+ d_et.getEntries(m, c, compat, gen);
+ for( unsigned i=0; i<compat.size(); i++) {
+ if( d_status[compat[i]]==status_unk ){
+ if( d_value[compat[i]]!=v ){
+ d_status[compat[i]] = status_non_redundant;
+ }
+ }
+ }
+ for( unsigned i=0; i<gen.size(); i++) {
+ if( d_status[gen[i]]==status_unk ){
+ if( d_value[gen[i]]==v ){
+ d_status[gen[i]] = status_redundant;
+ }
+ }
+ }
+ d_status.push_back( status_unk );
+ }
+ d_et.addEntry(m, c, v, newIndex);
+ d_cond.push_back(c);
+ d_value.push_back(v);
+ return true;
+ }else{
+ return false;
+ }
+}
+
+Node Def::evaluate( FullModelChecker * m, std::vector<Node> inst ) {
+ int gindex = d_et.getGeneralizationIndex(m, inst);
+ if (gindex!=-1) {
+ return d_value[gindex];
+ }else{
+ return Node::null();
+ }
+}
+
+int Def::getGeneralizationIndex( FullModelChecker * m, std::vector<Node> inst ) {
+ return d_et.getGeneralizationIndex(m, inst);
+}
+
+void Def::simplify(FullModelChecker * m) {
+ d_has_simplified = true;
+ std::vector< Node > cond;
+ cond.insert( cond.end(), d_cond.begin(), d_cond.end() );
+ d_cond.clear();
+ std::vector< Node > value;
+ value.insert( value.end(), d_value.begin(), d_value.end() );
+ d_value.clear();
+ d_et.reset();
+ for (unsigned i=0; i<d_status.size(); i++) {
+ if( d_status[i]!=status_redundant ){
+ addEntry(m, cond[i], value[i]);
+ }
+ }
+ d_status.clear();
+}
+
+void Def::debugPrint(const char * tr, Node op, FullModelChecker * m) {
+ if (!op.isNull()) {
+ Trace(tr) << "Model for " << op << " : " << std::endl;
+ }
+ for( unsigned i=0; i<d_cond.size(); i++) {
+ //print the condition
+ if (!op.isNull()) {
+ Trace(tr) << op;
+ }
+ m->debugPrintCond(tr, d_cond[i], true);
+ Trace(tr) << " -> ";
+ m->debugPrint(tr, d_value[i]);
+ Trace(tr) << std::endl;
+ }
+}
+
+
+FullModelChecker::FullModelChecker(context::Context* c, QuantifiersEngine* qe) :
+QModelBuilder( c, qe ){
+ d_true = NodeManager::currentNM()->mkConst(true);
+ d_false = NodeManager::currentNM()->mkConst(false);
+}
+
+
+void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
+ d_addedLemmas = 0;
+ FirstOrderModel* fm = (FirstOrderModel*)m;
+ if( fullModel ){
+ //make function values
+ for( std::map< Node, std::vector< Node > >::iterator it = m->d_uf_terms.begin(); it != m->d_uf_terms.end(); ++it ){
+ m->d_uf_models[ it->first ] = getFunctionValue( fm, it->first, "$x" );
+ }
+ TheoryEngineModelBuilder::processBuildModel( m, fullModel );
+ //mark that the model has been set
+ fm->markModelSet();
+ }else{
+ Trace("fmc") << "---Full Model Check reset() " << std::endl;
+ for( std::map<Node, Def * >::iterator it = d_models.begin(); it != d_models.end(); ++it ){
+ it->second->reset();
+ }
+ d_quant_models.clear();
+ d_models_init.clear();
+ d_rep_ids.clear();
+ d_model_basis_rep.clear();
+ d_star_insts.clear();
+ //process representatives
+ for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin();
+ it != fm->d_rep_set.d_type_reps.end(); ++it ){
+ if( it->first.isSort() ){
+ Trace("fmc") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
+ Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(it->first);
+ Node rmbt = fm->getRepresentative(mbt);
+ int mbt_index = -1;
+ Trace("fmc") << " Model basis term : " << mbt << std::endl;
+ for( size_t a=0; a<it->second.size(); a++ ){
+ //Node r2 = ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getRepresentative( it->second[a] );
+ //Node ir = ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getInternalRepresentative( it->second[a], Node::null(), 0 );
+ Node r = fm->getRepresentative( it->second[a] );
+ std::vector< Node > eqc;
+ ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getEquivalenceClass( r, eqc );
+ Trace("fmc-model-debug") << " " << (it->second[a]==r) << (r==mbt);
+ Trace("fmc-model-debug") << " : " << it->second[a] << " : " << r << " : ";
+ //Trace("fmc-model-debug") << r2 << " : " << ir << " : ";
+ Trace("fmc-model-debug") << " {";
+ //find best selection for representative
+ for( size_t i=0; i<eqc.size(); i++ ){
+ Trace("fmc-model-debug") << eqc[i] << ", ";
+ }
+ Trace("fmc-model-debug") << "}" << std::endl;
+
+ //if this is the model basis eqc, replace with actual model basis term
+ if (r==rmbt || (mbt_index==-1 && a==(it->second.size()-1))) {
+ d_model_basis_rep[it->first] = r;
+ r = mbt;
+ mbt_index = a;
+ }
+ d_rep_ids[it->first][r] = (int)a;
+ }
+ Trace("fmc-model-debug") << std::endl;
+
+ if (mbt_index==-1) {
+ std::cout << " WARNING: model basis term is not a representative!" << std::endl;
+ exit(0);
+ }else{
+ Trace("fmc") << "Star index for " << it->first << " is " << mbt_index << std::endl;
+ }
+ }
+ }
+ }
+}
+
+Node FullModelChecker::getRepresentative(FirstOrderModel * fm, Node n) {
+ //Assert( fm->hasTerm(n) );
+ TypeNode tn = n.getType();
+ if( tn.isBoolean() ){
+ return fm->areEqual(n, d_true) ? d_true : d_false;
+ }else{
+ Node r = fm->getRepresentative(n);
+ if (r==d_model_basis_rep[tn]) {
+ r = d_qe->getTermDatabase()->getModelBasisTerm(tn);
+ }
+ return r;
+ }
+}
+
+struct ModelBasisArgSort
+{
+ std::vector< Node > d_terms;
+ bool operator() (int i,int j) {
+ return (d_terms[i].getAttribute(ModelBasisArgAttribute()) <
+ d_terms[j].getAttribute(ModelBasisArgAttribute()) );
+ }
+};
+
+void FullModelChecker::addEntry( FirstOrderModel * fm, Node op, Node c, Node v,
+ std::vector< Node > & conds,
+ std::vector< Node > & values,
+ std::vector< Node > & entry_conds ) {
+ std::vector< Node > children;
+ std::vector< Node > entry_children;
+ children.push_back(op);
+ entry_children.push_back(op);
+ bool hasNonStar = false;
+ for( unsigned i=0; i<c.getNumChildren(); i++) {
+ Node ri = getRepresentative(fm, c[i]);
+ children.push_back(ri);
+ if (isModelBasisTerm(ri)) {
+ ri = getStar( ri.getType() );
+ }else{
+ hasNonStar = true;
+ }
+ entry_children.push_back(ri);
+ }
+ Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children );
+ Node nv = getRepresentative(fm, v);
+ Node en = (useSimpleModels() && hasNonStar) ? n : NodeManager::currentNM()->mkNode( APPLY_UF, entry_children );
+ if( std::find(conds.begin(), conds.end(), n )==conds.end() ){
+ Trace("fmc-model-debug") << "- add " << n << " -> " << nv << " (entry is " << en << ")" << std::endl;
+ conds.push_back(n);
+ values.push_back(nv);
+ entry_conds.push_back(en);
+ }
+}
+
+Def * FullModelChecker::getModel(FirstOrderModel * fm, Node op) {
+ if( d_models_init.find(op)==d_models_init.end() ){
+ if( d_models.find(op)==d_models.end() ){
+ d_models[op] = new Def;
+ }
+ //reset the model
+ d_models[op]->reset();
+
+ std::vector< Node > conds;
+ std::vector< Node > values;
+ std::vector< Node > entry_conds;
+ Trace("fmc-model-debug") << fm->d_uf_terms[op].size() << " model values for " << op << " ... " << std::endl;
+ for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){
+ Node r = getRepresentative(fm, fm->d_uf_terms[op][i]);
+ Trace("fmc-model-debug") << fm->d_uf_terms[op][i] << " -> " << r << std::endl;
+ }
+ Trace("fmc-model-debug") << std::endl;
+ //initialize the model
+ /*
+ for( int j=0; j<2; j++ ){
+ for( int k=1; k>=0; k-- ){
+ Trace("fmc-model-debug")<< "Set values " << j << " " << k << " : " << std::endl;
+ for( std::map< Node, Node >::iterator it = fm->d_uf_model_gen[op].d_set_values[j][k].begin();
+ it != fm->d_uf_model_gen[op].d_set_values[j][k].end(); ++it ){
+ Trace("fmc-model-debug") << " process : " << it->first << " -> " << it->second << std::endl;
+ if( j==1 ){
+ addEntry(fm, op, it->first, it->second, conds, values, entry_conds);
+ }
+ }
+ }
+ }
+ */
+ for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){
+ Node n = fm->d_uf_terms[op][i];
+ if( !n.getAttribute(NoMatchAttribute()) ){
+ addEntry(fm, op, n, n, conds, values, entry_conds);
+ }
+ }
+ Node nmb = d_qe->getTermDatabase()->getModelBasisOpTerm(op);
+ //add default value
+ if( fm->hasTerm( nmb ) ){
+ Trace("fmc-model-debug") << "Add default " << nmb << std::endl;
+ addEntry(fm, op, nmb, nmb, conds, values, entry_conds);
+ }else{
+ Node vmb = getSomeDomainElement( fm, nmb.getType() );
+ Trace("fmc-model-debug") << "Add default to default representative " << nmb << " ";
+ Trace("fmc-model-debug") << fm->d_rep_set.d_type_reps[nmb.getType()].size() << std::endl;
+ addEntry(fm, op, nmb, vmb, conds, values, entry_conds);
+ }
+
+ //sort based on # default arguments
+ std::vector< int > indices;
+ ModelBasisArgSort mbas;
+ for (int i=0; i<(int)conds.size(); i++) {
+ d_qe->getTermDatabase()->computeModelBasisArgAttribute( conds[i] );
+ mbas.d_terms.push_back(conds[i]);
+ indices.push_back(i);
+ }
+ std::sort( indices.begin(), indices.end(), mbas );
+
+
+ for (int i=0; i<(int)indices.size(); i++) {
+ d_models[op]->addEntry(this, entry_conds[indices[i]], values[indices[i]]);
+ }
+ d_models[op]->debugPrint("fmc-model", op, this);
+ Trace("fmc-model") << std::endl;
+
+ d_models[op]->simplify( this );
+ Trace("fmc-model-simplify") << "After simplification : " << std::endl;
+ d_models[op]->debugPrint("fmc-model-simplify", op, this);
+ Trace("fmc-model-simplify") << std::endl;
+
+ d_models_init[op] = true;
+ }
+ return d_models[op];
+}
+
+
+bool FullModelChecker::isStar(Node n) {
+ return n==getStar(n.getType());
+}
+
+bool FullModelChecker::isModelBasisTerm(Node n) {
+ return n==getModelBasisTerm(n.getType());
+}
+
+Node FullModelChecker::getModelBasisTerm(TypeNode tn) {
+ return d_qe->getTermDatabase()->getModelBasisTerm(tn);
+}
+
+void FullModelChecker::debugPrintCond(const char * tr, Node n, bool dispStar) {
+ Trace(tr) << "(";
+ for( unsigned j=0; j<n.getNumChildren(); j++) {
+ if( j>0 ) Trace(tr) << ", ";
+ debugPrint(tr, n[j], dispStar);
+ }
+ Trace(tr) << ")";
+}
+
+void FullModelChecker::debugPrint(const char * tr, Node n, bool dispStar) {
+ if( n.isNull() ){
+ Trace(tr) << "null";
+ }
+ else if(isStar(n) && dispStar) {
+ Trace(tr) << "*";
+ }else{
+ TypeNode tn = n.getType();
+ if( d_rep_ids.find(tn)!=d_rep_ids.end() ){
+ if (d_rep_ids[tn].find(n)!=d_rep_ids[tn].end()) {
+ Trace(tr) << d_rep_ids[tn][n];
+ }else{
+ Trace(tr) << n;
+ }
+ }else{
+ Trace(tr) << n;
+ }
+ }
+}
+
+
+bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort, int & lemmas ) {
+ Trace("fmc") << "Full model check " << f << ", effort = " << effort << "..." << std::endl;
+ if (effort==0) {
+ //register the quantifier
+ if (d_quant_cond.find(f)==d_quant_cond.end()) {
+ std::vector< TypeNode > types;
+ for(unsigned i=0; i<f[0].getNumChildren(); i++){
+ types.push_back(f[0][i].getType());
+ d_quant_var_id[f][f[0][i]] = i;
+ }
+ TypeNode typ = NodeManager::currentNM()->mkFunctionType( types, NodeManager::currentNM()->booleanType() );
+ Node op = NodeManager::currentNM()->mkSkolem( "fmc_$$", typ, "op created for full-model checking" );
+ d_quant_cond[f] = op;
+ }
+
+ //model check the quantifier
+ doCheck(fm, f, d_quant_models[f], f[1]);
+ Trace("fmc") << "Definition for quantifier " << f << " is : " << std::endl;
+ d_quant_models[f].debugPrint("fmc", Node::null(), this);
+ Trace("fmc") << std::endl;
+ //consider all entries going to false
+ for (unsigned i=0; i<d_quant_models[f].d_cond.size(); i++) {
+ if( d_quant_models[f].d_value[i]!=d_true) {
+ Trace("fmc-inst") << "Instantiate based on " << d_quant_models[f].d_cond[i] << "..." << std::endl;
+ bool hasStar = false;
+ std::vector< Node > inst;
+ for (unsigned j=0; j<d_quant_models[f].d_cond[i].getNumChildren(); j++) {
+ if (isStar(d_quant_models[f].d_cond[i][j])) {
+ hasStar = true;
+ inst.push_back(getModelBasisTerm(d_quant_models[f].d_cond[i][j].getType()));
+ }else{
+ inst.push_back(d_quant_models[f].d_cond[i][j]);
+ }
+ }
+ bool addInst = true;
+ if( hasStar ){
+ //try obvious (specified by inst)
+ Node ev = d_quant_models[f].evaluate(this, inst);
+ if (ev==d_true) {
+ addInst = false;
+ }
+ }else{
+ //for debugging
+ if (Trace.isOn("fmc-test-inst")) {
+ Node ev = d_quant_models[f].evaluate(this, inst);
+ if( ev==d_true ){
+ std::cout << "WARNING: instantiation was true! " << f << " " << d_quant_models[f].d_cond[i] << std::endl;
+ exit(0);
+ }else{
+ Trace("fmc-test-inst") << "...instantiation evaluated to false." << std::endl;
+ }
+ }
+ }
+ if( addInst ){
+ InstMatch m;
+ for( unsigned j=0; j<inst.size(); j++) {
+ m.set( d_qe, f, j, inst[j] );
+ }
+ if( d_qe->addInstantiation( f, m ) ){
+ lemmas++;
+ }else{
+ //this can happen if evaluation is unknown
+ //might try it next effort level
+ d_star_insts[f].push_back(i);
+ }
+ }else{
+ //might try it next effort level
+ d_star_insts[f].push_back(i);
+ }
+ }
+ }
+ }else{
+ if (!d_star_insts[f].empty()) {
+ Trace("fmc-exh") << "Exhaustive instantiate " << f << std::endl;
+ Trace("fmc-exh") << "Definition was : " << std::endl;
+ d_quant_models[f].debugPrint("fmc-exh", Node::null(), this);
+ Trace("fmc-exh") << std::endl;
+ Def temp;
+ //simplify the exceptions?
+ for( int i=(d_star_insts[f].size()-1); i>=0; i--) {
+ //get witness for d_star_insts[f][i]
+ int j = d_star_insts[f][i];
+ if( temp.addEntry( this, d_quant_models[f].d_cond[j], d_quant_models[f].d_value[j] ) ){
+ int lem = exhaustiveInstantiate(fm, f, d_quant_models[f].d_cond[j], j );
+ if( lem==-1 ){
+ //something went wrong, resort to exhaustive instantiation
+ return false;
+ }else{
+ lemmas += lem;
+ }
+ }
+ }
+ }
+ }
+ return true;
+}
+
+int FullModelChecker::exhaustiveInstantiate(FirstOrderModel * fm, Node f, Node c, int c_index) {
+ int addedLemmas = 0;
+ RepSetIterator riter( &(fm->d_rep_set) );
+ Trace("fmc-exh") << "Exhaustive instantiate based on index " << c_index << " : " << c << " ";
+ debugPrintCond("fmc-exh", c, true);
+ Trace("fmc-exh")<< std::endl;
+ if( riter.setQuantifier( d_qe, f ) ){
+ std::vector< RepDomain > dom;
+ for (unsigned i=0; i<c.getNumChildren(); i++) {
+ TypeNode tn = c[i].getType();
+ if( d_rep_ids.find(tn)!=d_rep_ids.end() ){
+ //RepDomain rd;
+ if( isStar(c[i]) ){
+ //add the full range
+ //for( std::map< Node, int >::iterator it = d_rep_ids[tn].begin();
+ // it != d_rep_ids[tn].end(); ++it ){
+ // rd.push_back(it->second);
+ //}
+ }else{
+ if (d_rep_ids[tn].find(c[i])!=d_rep_ids[tn].end()) {
+ //rd.push_back(d_rep_ids[tn][c[i]]);
+ riter.d_domain[i].clear();
+ riter.d_domain[i].push_back(d_rep_ids[tn][c[i]]);
+ }else{
+ return -1;
+ }
+ }
+ //dom.push_back(rd);
+ }else{
+ return -1;
+ }
+ }
+ //riter.setDomain(dom);
+ //now do full iteration
+ while( !riter.isFinished() ){
+ Trace("fmc-exh-debug") << "Inst : ";
+ std::vector< Node > inst;
+ for( int i=0; i<riter.getNumTerms(); i++ ){
+ //m.set( d_quantEngine, f, riter.d_index_order[i], riter.getTerm( i ) );
+ Node r = getRepresentative( fm, riter.getTerm( i ) );
+ debugPrint("fmc-exh-debug", r);
+ Trace("fmc-exh-debug") << " ";
+ inst.push_back(r);
+ }
+
+ int ev_index = d_quant_models[f].getGeneralizationIndex(this, inst);
+ Trace("fmc-exh-debug") << ", index = " << ev_index;
+ Node ev = ev_index==-1 ? Node::null() : d_quant_models[f].d_value[ev_index];
+ if (ev!=d_true) {
+ InstMatch m;
+ for( int i=0; i<riter.getNumTerms(); i++ ){
+ m.set( d_qe, f, i, riter.getTerm( i ) );
+ }
+ Trace("fmc-exh-debug") << ", add!";
+ //add as instantiation
+ if( d_qe->addInstantiation( f, m ) ){
+ addedLemmas++;
+ }
+ }
+ Trace("fmc-exh-debug") << std::endl;
+ riter.increment();
+ }
+ }
+ return addedLemmas;
+}
+
+void FullModelChecker::doCheck(FirstOrderModel * fm, Node f, Def & d, Node n ) {
+ Trace("fmc-debug") << "Check " << n << " " << n.getKind() << std::endl;
+ if( n.getKind() == kind::BOUND_VARIABLE ){
+ d.addEntry(this, mkCondDefault(f), n);
+ Trace("fmc-debug") << "Done with " << n << " " << n.getKind() << std::endl;
+ }
+ else if( n.getNumChildren()==0 ){
+ Node r = n;
+ if( !fm->hasTerm(n) ){
+ r = getSomeDomainElement( fm, n.getType() );
+ }
+ r = getRepresentative(fm, r);
+ d.addEntry(this, mkCondDefault(f), r);
+ }
+ else if( n.getKind() == kind::NOT ){
+ //just do directly
+ doCheck( fm, f, d, n[0] );
+ doNegate( d );
+ }
+ else if( n.getKind() == kind::FORALL ){
+ d.addEntry(this, mkCondDefault(f), Node::null());
+ }
+ else{
+ std::vector< int > var_ch;
+ std::vector< Def > children;
+ for( int i=0; i<(int)n.getNumChildren(); i++) {
+ Def dc;
+ doCheck(fm, f, dc, n[i]);
+ children.push_back(dc);
+ if( n[i].getKind() == kind::BOUND_VARIABLE ){
+ var_ch.push_back(i);
+ }
+ }
+
+ if( n.getKind()==APPLY_UF ){
+ Trace("fmc-debug") << "Do uninterpreted compose " << n << std::endl;
+ //uninterpreted compose
+ doUninterpretedCompose( fm, f, d, n.getOperator(), children );
+ } else {
+ if( !var_ch.empty() ){
+ if( n.getKind()==EQUAL ){
+ if( var_ch.size()==2 ){
+ Trace("fmc-debug") << "Do variable equality " << n << std::endl;
+ doVariableEquality( fm, f, d, n );
+ }else{
+ Trace("fmc-debug") << "Do variable relation " << n << std::endl;
+ doVariableRelation( fm, f, d, var_ch[0]==0 ? children[1] : children[0], var_ch[0]==0 ? n[0] : n[1] );
+ }
+ }else{
+ std::cout << "Don't know how to check " << n << std::endl;
+ exit(0);
+ }
+ }else{
+ Trace("fmc-debug") << "Do interpreted compose " << n << std::endl;
+ std::vector< Node > cond;
+ mkCondDefaultVec(f, cond);
+ std::vector< Node > val;
+ //interpreted compose
+ doInterpretedCompose( fm, f, d, n, children, 0, cond, val );
+ }
+ }
+ d.simplify(this);
+ }
+ Trace("fmc-debug") << "Definition for " << n << " is : " << std::endl;
+ d.debugPrint("fmc-debug", Node::null(), this);
+ Trace("fmc-debug") << std::endl;
+}
+
+void FullModelChecker::doNegate( Def & dc ) {
+ for (unsigned i=0; i<dc.d_cond.size(); i++) {
+ if (!dc.d_value[i].isNull()) {
+ dc.d_value[i] = dc.d_value[i]==d_true ? d_false : d_true;
+ }
+ }
+}
+
+void FullModelChecker::doVariableEquality( FirstOrderModel * fm, Node f, Def & d, Node eq ) {
+ std::vector<Node> cond;
+ mkCondDefaultVec(f, cond);
+ if (eq[0]==eq[1]){
+ d.addEntry(this, mkCond(cond), d_true);
+ }else{
+ int j = getVariableId(f, eq[0]);
+ int k = getVariableId(f, eq[1]);
+ TypeNode tn = eq[0].getType();
+ if( !fm->d_rep_set.hasType( tn ) ){
+ getSomeDomainElement( fm, tn ); //to verify the type is initialized
+ }
+ for (unsigned i=0; i<fm->d_rep_set.d_type_reps[tn].size(); i++) {
+ Node r = getRepresentative( fm, fm->d_rep_set.d_type_reps[tn][i] );
+ cond[j+1] = r;
+ cond[k+1] = r;
+ d.addEntry( this, mkCond(cond), d_true);
+ }
+ d.addEntry(this, mkCondDefault(f), d_false);
+ }
+}
+
+void FullModelChecker::doVariableRelation( FirstOrderModel * fm, Node f, Def & d, Def & dc, Node v) {
+ int j = getVariableId(f, v);
+ for (unsigned i=0; i<dc.d_cond.size(); i++) {
+ Node val = dc.d_value[i];
+ if( dc.d_cond[i][j]!=val ){
+ if (isStar(dc.d_cond[i][j])) {
+ std::vector<Node> cond;
+ mkCondVec(dc.d_cond[i],cond);
+ cond[j+1] = val;
+ d.addEntry(this, mkCond(cond), d_true);
+ cond[j+1] = getStar(val.getType());
+ d.addEntry(this, mkCond(cond), d_false);
+ }else{
+ d.addEntry( this, dc.d_cond[i], d_false);
+ }
+ }else{
+ d.addEntry( this, dc.d_cond[i], d_true);
+ }
+ }
+}
+
+void FullModelChecker::doUninterpretedCompose( FirstOrderModel * fm, Node f, Def & d, Node op, std::vector< Def > & dc ) {
+ getModel(fm, op);
+ Trace("fmc-uf-debug") << "Definition : " << std::endl;
+ d_models[op]->debugPrint("fmc-uf-debug", op, this);
+ Trace("fmc-uf-debug") << std::endl;
+
+ std::vector< Node > cond;
+ mkCondDefaultVec(f, cond);
+ std::vector< Node > val;
+ doUninterpretedCompose( fm, f, op, d, dc, 0, cond, val);
+}
+
+void FullModelChecker::doUninterpretedCompose( FirstOrderModel * fm, Node f, Node op, Def & d,
+ std::vector< Def > & dc, int index,
+ std::vector< Node > & cond, std::vector<Node> & val ) {
+ Trace("fmc-uf-process") << "process at " << index << std::endl;
+ for( unsigned i=1; i<cond.size(); i++) {
+ debugPrint("fmc-uf-process", cond[i], true);
+ Trace("fmc-uf-process") << " ";
+ }
+ Trace("fmc-uf-process") << std::endl;
+ if (index==(int)dc.size()) {
+ //we have an entry, now do actual compose
+ std::map< int, Node > entries;
+ doUninterpretedCompose2( fm, f, entries, 0, cond, val, d_models[op]->d_et);
+ //add them to the definition
+ for( unsigned e=0; e<d_models[op]->d_cond.size(); e++ ){
+ if ( entries.find(e)!=entries.end() ){
+ d.addEntry(this, entries[e], d_models[op]->d_value[e] );
+ }
+ }
+ }else{
+ for (unsigned i=0; i<dc[index].d_cond.size(); i++) {
+ if (isCompat(cond, dc[index].d_cond[i])!=0) {
+ std::vector< Node > new_cond;
+ new_cond.insert(new_cond.end(), cond.begin(), cond.end());
+ if( doMeet(new_cond, dc[index].d_cond[i]) ){
+ Trace("fmc-uf-process") << "index " << i << " succeeded meet." << std::endl;
+ val.push_back(dc[index].d_value[i]);
+ doUninterpretedCompose(fm, f, op, d, dc, index+1, new_cond, val);
+ val.pop_back();
+ }else{
+ Trace("fmc-uf-process") << "index " << i << " failed meet." << std::endl;
+ }
+ }
+ }
+ }
+}
+
+void FullModelChecker::doUninterpretedCompose2( FirstOrderModel * fm, Node f,
+ std::map< int, Node > & entries, int index,
+ std::vector< Node > & cond, std::vector< Node > & val,
+ EntryTrie & curr ) {
+ Trace("fmc-uf-process") << "compose " << index << std::endl;
+ for( unsigned i=1; i<cond.size(); i++) {
+ debugPrint("fmc-uf-process", cond[i], true);
+ Trace("fmc-uf-process") << " ";
+ }
+ Trace("fmc-uf-process") << std::endl;
+ if (index==(int)val.size()) {
+ Node c = mkCond(cond);
+ Trace("fmc-uf-entry") << "Entry : " << c << " -> index[" << curr.d_data << "]" << std::endl;
+ entries[curr.d_data] = c;
+ }else{
+ Node v = val[index];
+ bool bind_var = false;
+ if( v.getKind()==kind::BOUND_VARIABLE ){
+ int j = getVariableId(f, v);
+ Trace("fmc-uf-process") << v << " is variable #" << j << std::endl;
+ if (!isStar(cond[j+1])) {
+ v = cond[j+1];
+ }else{
+ bind_var = true;
+ }
+ }
+ if (bind_var) {
+ Trace("fmc-uf-process") << "bind variable..." << std::endl;
+ int j = getVariableId(f, v);
+ for (std::map<Node, EntryTrie>::iterator it = curr.d_child.begin(); it != curr.d_child.end(); ++it) {
+ cond[j+1] = it->first;
+ doUninterpretedCompose2(fm, f, entries, index+1, cond, val, it->second);
+ }
+ cond[j+1] = getStar(v.getType());
+ }else{
+ if (curr.d_child.find(v)!=curr.d_child.end()) {
+ Trace("fmc-uf-process") << "follow value..." << std::endl;
+ doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[v]);
+ }
+ Node st = getStar(v.getType());
+ if (curr.d_child.find(st)!=curr.d_child.end()) {
+ Trace("fmc-uf-process") << "follow star..." << std::endl;
+ doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[st]);
+ }
+ }
+ }
+}
+
+void FullModelChecker::doInterpretedCompose( FirstOrderModel * fm, Node f, Def & d, Node n,
+ std::vector< Def > & dc, int index,
+ std::vector< Node > & cond, std::vector<Node> & val ) {
+ if ( index==(int)dc.size() ){
+ Node c = mkCond(cond);
+ Node v = evaluateInterpreted(n, val);
+ d.addEntry(this, c, v);
+ }
+ else {
+ TypeNode vtn = n.getType();
+ for (unsigned i=0; i<dc[index].d_cond.size(); i++) {
+ if (isCompat(cond, dc[index].d_cond[i])!=0) {
+ std::vector< Node > new_cond;
+ new_cond.insert(new_cond.end(), cond.begin(), cond.end());
+ if( doMeet(new_cond, dc[index].d_cond[i]) ){
+ bool process = true;
+ if (vtn.isBoolean()) {
+ //short circuit
+ if( (n.getKind()==OR && dc[index].d_value[i]==d_true) ||
+ (n.getKind()==AND && dc[index].d_value[i]==d_false) ){
+ Node c = mkCond(new_cond);
+ d.addEntry(this, c, dc[index].d_value[i]);
+ process = false;
+ }
+ }
+ if (process) {
+ val.push_back(dc[index].d_value[i]);
+ doInterpretedCompose(fm, f, d, n, dc, index+1, new_cond, val);
+ val.pop_back();
+ }
+ }
+ }
+ }
+ }
+}
+
+int FullModelChecker::isCompat( std::vector< Node > & cond, Node c ) {
+ Assert(cond.size()==c.getNumChildren()+1);
+ for (unsigned i=1; i<cond.size(); i++) {
+ if( cond[i]!=c[i-1] && !isStar(cond[i]) && !isStar(c[i-1]) ) {
+ return 0;
+ }
+ }
+ return 1;
+}
+
+bool FullModelChecker::doMeet( std::vector< Node > & cond, Node c ) {
+ Assert(cond.size()==c.getNumChildren()+1);
+ for (unsigned i=1; i<cond.size(); i++) {
+ if( cond[i]!=c[i-1] ) {
+ if( isStar(cond[i]) ){
+ cond[i] = c[i-1];
+ }else if( !isStar(c[i-1]) ){
+ return false;
+ }
+ }
+ }
+ return true;
+}
+
+Node FullModelChecker::mkCond( std::vector< Node > & cond ) {
+ return NodeManager::currentNM()->mkNode(APPLY_UF, cond);
+}
+
+Node FullModelChecker::mkCondDefault( Node f) {
+ std::vector< Node > cond;
+ mkCondDefaultVec(f, cond);
+ return mkCond(cond);
+}
+
+Node FullModelChecker::getStar(TypeNode tn) {
+ if( d_type_star.find(tn)==d_type_star.end() ){
+ Node st = NodeManager::currentNM()->mkSkolem( "star_$$", tn, "skolem created for full-model checking" );
+ d_type_star[tn] = st;
+ }
+ return d_type_star[tn];
+}
+
+Node FullModelChecker::getSomeDomainElement(FirstOrderModel * fm, TypeNode tn){
+ //check if there is even any domain elements at all
+ if (!fm->d_rep_set.hasType(tn)) {
+ Trace("fmc-model-debug") << "Must create domain element for " << tn << "..." << std::endl;
+ Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(tn);
+ fm->d_rep_set.d_type_reps[tn].push_back(mbt);
+ }else if( fm->d_rep_set.d_type_reps[tn].size()==0 ){
+ Message() << "empty reps" << std::endl;
+ exit(0);
+ }
+ return fm->d_rep_set.d_type_reps[tn][0];
+}
+
+void FullModelChecker::mkCondDefaultVec( Node f, std::vector< Node > & cond ) {
+ //get function symbol for f
+ cond.push_back(d_quant_cond[f]);
+ for (unsigned i=0; i<f[0].getNumChildren(); i++) {
+ Node ts = getStar( f[0][i].getType() );
+ cond.push_back(ts);
+ }
+}
+
+void FullModelChecker::mkCondVec( Node n, std::vector< Node > & cond ) {
+ cond.push_back(n.getOperator());
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ cond.push_back( n[i] );
+ }
+}
+
+Node FullModelChecker::evaluateInterpreted( Node n, std::vector< Node > & vals ) {
+ if( n.getKind()==EQUAL ){
+ return vals[0]==vals[1] ? d_true : d_false;
+ }else if( n.getKind()==ITE ){
+ if( vals[0]==d_true ){
+ return vals[1];
+ }else if( vals[0]==d_false ){
+ return vals[2];
+ }else{
+ return vals[1]==vals[2] ? vals[1] : Node::null();
+ }
+ }else if( n.getKind()==AND || n.getKind()==OR ){
+ bool isNull = false;
+ for (unsigned i=0; i<vals.size(); i++) {
+ if((vals[i]==d_true && n.getKind()==OR) || (vals[i]==d_false && n.getKind()==AND)) {
+ return vals[i];
+ }else if( vals[i].isNull() ){
+ isNull = true;
+ }
+ }
+ return isNull ? Node::null() : vals[0];
+ }else{
+ std::vector<Node> children;
+ if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+ children.push_back( n.getOperator() );
+ }
+ for (unsigned i=0; i<vals.size(); i++) {
+ if( vals[i].isNull() ){
+ return Node::null();
+ }else{
+ children.push_back( vals[i] );
+ }
+ }
+ Node nc = NodeManager::currentNM()->mkNode(n.getKind(), children);
+ Trace("fmc-eval") << "Evaluate " << nc << " to ";
+ nc = Rewriter::rewrite(nc);
+ Trace("fmc-eval") << nc << std::endl;
+ return nc;
+ }
+}
+
+bool FullModelChecker::useSimpleModels() {
+ return options::fmfFullModelCheckSimple();
+}
+
+Node FullModelChecker::getFunctionValue(FirstOrderModel * fm, Node op, const char* argPrefix ) {
+ getModel( fm, op );
+ TypeNode type = op.getType();
+ std::vector< Node > vars;
+ for( size_t i=0; i<type.getNumChildren()-1; i++ ){
+ std::stringstream ss;
+ ss << argPrefix << (i+1);
+ vars.push_back( NodeManager::currentNM()->mkBoundVar( ss.str(), type[i] ) );
+ }
+ Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, vars);
+ Node curr;
+ for( int i=(d_models[op]->d_cond.size()-1); i>=0; i--) {
+ Node v = fm->getRepresentative( d_models[op]->d_value[i] );
+ if( curr.isNull() ){
+ curr = v;
+ }else{
+ //make the condition
+ Node cond = d_models[op]->d_cond[i];
+ std::vector< Node > children;
+ for( unsigned j=0; j<cond.getNumChildren(); j++) {
+ if (!isStar(cond[j])){
+ Node c = fm->getRepresentative( cond[j] );
+ children.push_back( NodeManager::currentNM()->mkNode( EQUAL, vars[j], c ) );
+ }
+ }
+ Assert( !children.empty() );
+ Node cc = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( AND, children );
+ curr = NodeManager::currentNM()->mkNode( ITE, cc, v, curr );
+ }
+ }
+ curr = Rewriter::rewrite( curr );
+ return NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, curr);
+}
\ No newline at end of file diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h new file mode 100755 index 000000000..92c866ffd --- /dev/null +++ b/src/theory/quantifiers/full_model_check.h @@ -0,0 +1,151 @@ +/********************* */
+/*! \file full_model_check.h
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Full model check class
+ **/
+
+#ifndef FULL_MODEL_CHECK
+#define FULL_MODEL_CHECK
+
+#include "theory/quantifiers/model_builder.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+namespace fmcheck {
+
+
+class FullModelChecker;
+
+class EntryTrie
+{
+public:
+ EntryTrie() : d_data(-1){}
+ std::map<Node,EntryTrie> d_child;
+ int d_data;
+ void reset() { d_data = -1; d_child.clear(); }
+ void addEntry( FullModelChecker * m, Node c, Node v, int data, int index = 0 );
+ bool hasGeneralization( FullModelChecker * m, Node c, int index = 0 );
+ int getGeneralizationIndex( FullModelChecker * m, std::vector<Node> & inst, int index = 0 );
+ void getEntries( FullModelChecker * m, Node c, std::vector<int> & compat, std::vector<int> & gen, int index = 0, bool is_gen = true );
+ //if possible, get ground instance of c that evaluates to the entry
+ bool getWitness( FullModelChecker * m, FirstOrderModel * fm, Node c, std::vector<Node> & inst, int index = 0 );
+};
+
+
+class Def
+{
+public:
+ EntryTrie d_et;
+ //cond is APPLY_UF whose arguments are returned by FullModelChecker::getRepresentative
+ std::vector< Node > d_cond;
+ //value is returned by FullModelChecker::getRepresentative
+ std::vector< Node > d_value;
+private:
+ enum {
+ status_unk,
+ status_redundant,
+ status_non_redundant
+ };
+ std::vector< int > d_status;
+ bool d_has_simplified;
+public:
+ Def() : d_has_simplified(false){}
+ void reset() {
+ d_et.reset();
+ d_cond.clear();
+ d_value.clear();
+ d_status.clear();
+ d_has_simplified = false;
+ }
+ bool addEntry( FullModelChecker * m, Node c, Node v);
+ Node evaluate( FullModelChecker * m, std::vector<Node> inst );
+ int getGeneralizationIndex( FullModelChecker * m, std::vector<Node> inst );
+ void simplify( FullModelChecker * m );
+ void debugPrint(const char * tr, Node op, FullModelChecker * m);
+};
+
+
+class FullModelChecker : public QModelBuilder
+{
+protected:
+ Node d_true;
+ Node d_false;
+ std::map<TypeNode, std::map< Node, int > > d_rep_ids;
+ std::map<TypeNode, Node > d_model_basis_rep;
+ std::map<Node, Def * > d_models;
+ std::map<Node, Def > d_quant_models;
+ std::map<Node, bool > d_models_init;
+ std::map<Node, Node > d_quant_cond;
+ std::map<TypeNode, Node > d_type_star;
+ std::map<Node, std::map< Node, int > > d_quant_var_id;
+ std::map<Node, std::vector< int > > d_star_insts;
+ Node getRepresentative(FirstOrderModel * fm, Node n);
+ Node normalizeArgReps(FirstOrderModel * fm, Node op, Node n);
+ void addEntry( FirstOrderModel * fm, Node op, Node c, Node v,
+ std::vector< Node > & conds,
+ std::vector< Node > & values,
+ std::vector< Node > & entry_conds );
+ int exhaustiveInstantiate(FirstOrderModel * fm, Node f, Node c, int c_index);
+private:
+ void doCheck(FirstOrderModel * fm, Node f, Def & d, Node n );
+
+ void doNegate( Def & dc );
+ void doVariableEquality( FirstOrderModel * fm, Node f, Def & d, Node eq );
+ void doVariableRelation( FirstOrderModel * fm, Node f, Def & d, Def & dc, Node v);
+ void doUninterpretedCompose( FirstOrderModel * fm, Node f, Def & d, Node n, std::vector< Def > & dc );
+
+ void doUninterpretedCompose( FirstOrderModel * fm, Node f, Node op, Def & d,
+ std::vector< Def > & dc, int index,
+ std::vector< Node > & cond, std::vector<Node> & val );
+ void doUninterpretedCompose2( FirstOrderModel * fm, Node f,
+ std::map< int, Node > & entries, int index,
+ std::vector< Node > & cond, std::vector< Node > & val,
+ EntryTrie & curr);
+
+ void doInterpretedCompose( FirstOrderModel * fm, Node f, Def & d, Node n,
+ std::vector< Def > & dc, int index,
+ std::vector< Node > & cond, std::vector<Node> & val );
+ int isCompat( std::vector< Node > & cond, Node c );
+ bool doMeet( std::vector< Node > & cond, Node c );
+ Node mkCond( std::vector< Node > & cond );
+ Node mkCondDefault( Node f );
+ void mkCondDefaultVec( Node f, std::vector< Node > & cond );
+ void mkCondVec( Node n, std::vector< Node > & cond );
+ Node evaluateInterpreted( Node n, std::vector< Node > & vals );
+public:
+ FullModelChecker( context::Context* c, QuantifiersEngine* qe );
+ ~FullModelChecker(){}
+
+ int getVariableId(Node f, Node n) { return d_quant_var_id[f][n]; }
+ bool isStar(Node n);
+ Node getStar(TypeNode tn);
+ Node getSomeDomainElement(FirstOrderModel * fm, TypeNode tn);
+ bool isModelBasisTerm(Node n);
+ Node getModelBasisTerm(TypeNode tn);
+ Def * getModel(FirstOrderModel * fm, Node op);
+
+ void debugPrintCond(const char * tr, Node n, bool dispStar = false);
+ void debugPrint(const char * tr, Node n, bool dispStar = false);
+
+ bool doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort, int & lemmas );
+
+ bool useSimpleModels();
+ Node getFunctionValue(FirstOrderModel * fm, Node op, const char* argPrefix );
+
+ /** process build model */
+ void processBuildModel(TheoryModel* m, bool fullModel);
+};
+
+}
+}
+}
+}
+
+#endif
diff --git a/src/theory/quantifiers/inst_gen.cpp b/src/theory/quantifiers/inst_gen.cpp index e495b39c0..192e58d7c 100644 --- a/src/theory/quantifiers/inst_gen.cpp +++ b/src/theory/quantifiers/inst_gen.cpp @@ -47,7 +47,7 @@ void InstGenProcess::addMatchValue( QuantifiersEngine* qe, Node f, Node val, Ins if( d_inst_trie[val].addInstMatch( qe, f, m, true ) ){ d_match_values.push_back( val ); d_matches.push_back( InstMatch( &m ) ); - qe->getModelEngine()->getModelBuilder()->d_instGenMatches++; + ((QModelBuilderIG*)qe->getModelEngine()->getModelBuilder())->d_instGenMatches++; } } } @@ -92,7 +92,7 @@ void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f, std::vecto //for each term we consider, calculate a current match for( size_t i=0; i<considerTerms.size(); i++ ){ Node n = considerTerms[i]; - bool isSelected = qe->getModelEngine()->getModelBuilder()->isTermSelected( n ); + bool isSelected = ((QModelBuilderIG*)qe->getModelEngine()->getModelBuilder())->isTermSelected( n ); bool hadSuccess CVC4_UNUSED = false; for( int t=(isSelected ? 0 : 1); t<2; t++ ){ if( t==0 || !n.getAttribute(NoMatchAttribute()) ){ @@ -193,7 +193,7 @@ void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f, std::vecto //process all values for( size_t i=0; i<considerTerms.size(); i++ ){ Node n = considerTerms[i]; - bool isSelected = qe->getModelEngine()->getModelBuilder()->isTermSelected( n ); + bool isSelected = ((QModelBuilderIG*)qe->getModelEngine()->getModelBuilder())->isTermSelected( n ); for( int t=(isSelected ? 0 : 1); t<2; t++ ){ //do not consider ground case if it is already congruent to another ground term if( t==0 || !n.getAttribute(NoMatchAttribute()) ){ diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index f6a0dad11..d4988f223 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -134,18 +134,27 @@ Node InstMatch::getValue( Node var ) const{ } } +Node InstMatch::get( QuantifiersEngine* qe, Node f, int i ) { + return get( qe->getTermDatabase()->getInstantiationConstant( f, i ) ); +} + void InstMatch::set(TNode var, TNode n){ Assert( !var.isNull() ); - if( !n.isNull() &&// For a strange use in inst_match.cpp InstMatchGeneratorSimple::addInstantiations - //var.getType() == n.getType() - !n.getType().isSubtypeOf( var.getType() ) ){ - Trace("inst-match-warn") << var.getAttribute(InstConstantAttribute()) << std::endl; - Trace("inst-match-warn") << var << " " << var.getType() << " " << n << " " << n.getType() << std::endl ; - Assert(false); + if (Trace.isOn("inst-match-warn")) { + // For a strange use in inst_match.cpp InstMatchGeneratorSimple::addInstantiations + if( !n.isNull() && !n.getType().isSubtypeOf( var.getType() ) ){ + Trace("inst-match-warn") << var.getAttribute(InstConstantAttribute()) << std::endl; + Trace("inst-match-warn") << var << " " << var.getType() << " " << n << " " << n.getType() << std::endl ; + } } + Assert( n.isNull() || n.getType().isSubtypeOf( var.getType() ) ); d_map[var] = n; } +void InstMatch::set( QuantifiersEngine* qe, Node f, int i, TNode n ) { + set( qe->getTermDatabase()->getInstantiationConstant( f, i ), n ); +} + /** add match m for quantifier f starting at index, take into account equalities q, return true if successful */ void InstMatchTrie::addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, int index, ImtIndexOrder* imtio ){ if( long(index)<long(f[0].getNumChildren()) && ( !imtio || long(index)<long(imtio->d_order.size()) ) ){ diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index 127f83c60..72447fd66 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -92,8 +92,11 @@ public: void erase(Node node){ d_map.erase(node); } /** get */ Node get( TNode var ) { return d_map[var]; } + Node get( QuantifiersEngine* qe, Node f, int i ); /** set */ void set(TNode var, TNode n); + void set( QuantifiersEngine* qe, Node f, int i, TNode n ); + /** size */ size_t size(){ return d_map.size(); } /* iterator */ std::map< Node, Node >::iterator begin(){ return d_map.begin(); }; diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index de7f2f373..105575c49 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -52,22 +52,28 @@ void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMat //we want to add the children of the NOT d_match_pattern = d_pattern[0]; } - if( d_match_pattern.getKind()==IFF || d_match_pattern.getKind()==EQUAL ){ - if( !d_match_pattern[0].hasAttribute(InstConstantAttribute()) ){ + if( d_match_pattern.getKind()==IFF || d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==GEQ ){ + if( !d_match_pattern[0].hasAttribute(InstConstantAttribute()) || + d_match_pattern[0].getKind()==INST_CONSTANT ){ Assert( d_match_pattern[1].hasAttribute(InstConstantAttribute()) ); + Node mp = d_match_pattern[1]; //swap sides Node pat = d_pattern; - d_pattern = NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), d_match_pattern[1], d_match_pattern[0] ); - d_pattern = pat.getKind()==NOT ? d_pattern.notNode() : d_pattern; - if( pat.getKind()!=NOT ){ //TEMPORARY until we do better implementation of disequality matching - d_match_pattern = d_match_pattern[1]; + if(d_match_pattern.getKind()==GEQ){ + d_pattern = NodeManager::currentNM()->mkNode( kind::GT, d_match_pattern[1], d_match_pattern[0] ); + d_pattern = d_pattern.negate(); }else{ - d_match_pattern = d_pattern[0][0]; + d_pattern = NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), d_match_pattern[1], d_match_pattern[0] ); } - }else if( !d_match_pattern[1].hasAttribute(InstConstantAttribute()) ){ + d_pattern = pat.getKind()==NOT ? d_pattern.negate() : d_pattern; + d_match_pattern = mp; + }else if( !d_match_pattern[1].hasAttribute(InstConstantAttribute()) || + d_match_pattern[1].getKind()==INST_CONSTANT ){ Assert( d_match_pattern[0].hasAttribute(InstConstantAttribute()) ); if( d_pattern.getKind()!=NOT ){ //TEMPORARY until we do better implementation of disequality matching d_match_pattern = d_match_pattern[0]; + }else if( d_match_pattern[1].getKind()==INST_CONSTANT ){ + d_match_pattern = d_match_pattern[0]; } } } @@ -96,17 +102,23 @@ void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMat //candidates will be all disequalities d_cg = new inst::CandidateGeneratorQELitDeq( qe, d_match_pattern ); } - }else if( d_pattern.getKind()==EQUAL || d_pattern.getKind()==IFF || d_pattern.getKind()==NOT ){ + }else if( d_pattern.getKind()==EQUAL || d_pattern.getKind()==IFF || + d_pattern.getKind()==GEQ || d_pattern.getKind()==GT || d_pattern.getKind()==NOT ){ Assert( d_matchPolicy==MATCH_GEN_DEFAULT ); if( d_pattern.getKind()==NOT ){ - Unimplemented("Disequal generator unimplemented"); + if (d_pattern[0][1].getKind()!=INST_CONSTANT) { + Unimplemented("Disequal generator unimplemented"); + }else{ + d_eq_class = d_pattern[0][1]; + } }else{ - Assert( Trigger::isAtomicTrigger( d_match_pattern ) ); - //we are matching only in a particular equivalence class - d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern.getOperator() ); //store the equivalence class that we will call d_cg->reset( ... ) on d_eq_class = d_pattern[1]; } + Assert( Trigger::isAtomicTrigger( d_match_pattern ) ); + //we are matching only in a particular equivalence class + d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern.getOperator() ); + }else if( Trigger::isAtomicTrigger( d_match_pattern ) ){ //if( d_matchPolicy==MATCH_GEN_EFFICIENT_E_MATCH ){ //Warning() << "Currently efficient e matching is not taken into account for quantifiers: " << d_pattern << std::endl; @@ -134,7 +146,7 @@ void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMat /** get match (not modulo equality) */ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngine* qe ){ Debug("matching") << "Matching " << t << " against pattern " << d_match_pattern << " (" - << m << ")" << ", " << d_children.size() << std::endl; + << m << ")" << ", " << d_children.size() << ", pattern is " << d_pattern << std::endl; Assert( !d_match_pattern.isNull() ); if( qe->d_optMatchIgnoreModelBasis && t.getAttribute(ModelBasisAttribute()) ){ return true; @@ -182,6 +194,36 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi } } } + //for relational matching + if( !d_eq_class.isNull() && d_eq_class.getKind()==INST_CONSTANT ){ + //also must fit match to equivalence class + bool pol = d_pattern.getKind()!=NOT; + Node pat = d_pattern.getKind()==NOT ? d_pattern[0] : d_pattern; + Node t_match; + if( pol ){ + if (pat.getKind()==GT) { + Node r = NodeManager::currentNM()->mkConst( Rational(-1) ); + t_match = NodeManager::currentNM()->mkNode(PLUS, t, r); + }else{ + t_match = t; + } + }else{ + if(pat.getKind()==EQUAL) { + Node r = NodeManager::currentNM()->mkConst( Rational(1) ); + t_match = NodeManager::currentNM()->mkNode(PLUS, t, r); + }else if( pat.getKind()==IFF ){ + t_match = NodeManager::currentNM()->mkConst( !q->areEqual( NodeManager::currentNM()->mkConst(true), t ) ); + }else if( pat.getKind()==GEQ ){ + Node r = NodeManager::currentNM()->mkConst( Rational(1) ); + t_match = NodeManager::currentNM()->mkNode(PLUS, t, r); + }else if( pat.getKind()==GT ){ + t_match = t; + } + } + if( !t_match.isNull() && !m.setMatch( q, d_eq_class, t_match ) ){ + success = false; + } + } if( success ){ //now, fit children into match //we will be requesting candidates for matching terms for each child @@ -286,7 +328,7 @@ void InstMatchGenerator::reset( Node eqc, QuantifiersEngine* qe ){ //we have a specific equivalence class in mind //we are producing matches for f(E) ~ t, where E is a non-ground vector of terms, and t is a ground term //just look in equivalence class of the RHS - d_cg->reset( d_eq_class ); + d_cg->reset( d_eq_class.getKind()==INST_CONSTANT ? Node::null() : d_eq_class ); } bool InstMatchGenerator::getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ){ @@ -306,7 +348,7 @@ bool InstMatchGenerator::getNextMatch( Node f, InstMatch& m, QuantifiersEngine* if( !success ){ //Debug("matching") << this << " failed, reset " << d_eq_class << std::endl; //we failed, must reset - reset( d_eq_class, qe ); + reset( d_eq_class.getKind()==INST_CONSTANT ? Node::null() : d_eq_class, qe ); } return success; } diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index 0e1266e0d..ef81d55a1 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -144,7 +144,11 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ) } if( gen ){ generateTriggers( f, effort, e, status ); + if( d_auto_gen_trigger[f].empty() && f.getNumChildren()==2 ){ + Trace("no-trigger") << "Could not find trigger for " << f << std::endl; + } } + //if( e==4 ){ // d_processed_trigger.clear(); // d_quantEngine->getEqualityQuery()->setLiberal( true ); diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 0b74cfc5e..79e36e9f5 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -33,6 +33,19 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; + +QModelBuilder::QModelBuilder( context::Context* c, QuantifiersEngine* qe ) : +TheoryEngineModelBuilder( qe->getTheoryEngine() ), d_curr_model( c, NULL ), d_qe( qe ){ + d_considerAxioms = true; + d_addedLemmas = 0; +} + + +bool QModelBuilder::optUseModel() { + return options::fmfModelBasedInst(); +} + + bool TermArgBasisTrie::addTerm2( FirstOrderModel* fm, Node n, int argIndex ){ if( argIndex<(int)n.getNumChildren() ){ Node r; @@ -53,13 +66,13 @@ bool TermArgBasisTrie::addTerm2( FirstOrderModel* fm, Node n, int argIndex ){ } } -ModelEngineBuilder::ModelEngineBuilder( context::Context* c, QuantifiersEngine* qe ) : -TheoryEngineModelBuilder( qe->getTheoryEngine() ), -d_qe( qe ), d_curr_model( c, NULL ){ - d_considerAxioms = true; +QModelBuilderIG::QModelBuilderIG( context::Context* c, QuantifiersEngine* qe ) : +QModelBuilder( c, qe ) { + } -void ModelEngineBuilder::debugModel( FirstOrderModel* fm ){ + +void QModelBuilderIG::debugModel( FirstOrderModel* fm ){ //debug the model: cycle through all instantiations for all quantifiers, report ones that are not true if( Trace.isOn("quant-model-warn") ){ for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ @@ -69,7 +82,7 @@ void ModelEngineBuilder::debugModel( FirstOrderModel* fm ){ vars.push_back( f[0][j] ); } RepSetIterator riter( &(fm->d_rep_set) ); - riter.setQuantifier( f ); + riter.setQuantifier( d_qe, f ); while( !riter.isFinished() ){ std::vector< Node > terms; for( int i=0; i<riter.getNumTerms(); i++ ){ @@ -88,14 +101,14 @@ void ModelEngineBuilder::debugModel( FirstOrderModel* fm ){ } } -void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) { +void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) { FirstOrderModel* fm = (FirstOrderModel*)m; if( fullModel ){ Assert( d_curr_model==fm ); //update models for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){ it->second.update( fm ); - Trace("model-func") << "ModelEngineBuilder: Make function value from tree " << it->first << std::endl; + Trace("model-func") << "QModelBuilder: Make function value from tree " << it->first << std::endl; //construct function values fm->d_uf_models[ it->first ] = it->second.getFunctionValue( "$x" ); } @@ -186,12 +199,13 @@ void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) { } } //construct the model if necessary - if( d_addedLemmas==0 || optExhInstNonInstGenQuant() ){ + if( d_addedLemmas==0 ){ //if no immediate exceptions, build the model // this model will be an approximation that will need to be tested via exhaustive instantiation Trace("model-engine-debug") << "Building model..." << std::endl; //build model for UF for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){ + Trace("model-engine-debug-uf") << "Building model for " << it->first << "..." << std::endl; constructModelUf( fm, it->first ); } /* @@ -211,7 +225,7 @@ void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) { } } -int ModelEngineBuilder::initializeQuantifier( Node f, Node fp ){ +int QModelBuilderIG::initializeQuantifier( Node f, Node fp ){ if( d_quant_basis_match_added.find( f )==d_quant_basis_match_added.end() ){ //create the basis match if necessary if( d_quant_basis_match.find( f )==d_quant_basis_match.end() ){ @@ -254,7 +268,7 @@ int ModelEngineBuilder::initializeQuantifier( Node f, Node fp ){ return 0; } -void ModelEngineBuilder::analyzeModel( FirstOrderModel* fm ){ +void QModelBuilderIG::analyzeModel( FirstOrderModel* fm ){ d_uf_model_constructed.clear(); //determine if any functions are constant for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){ @@ -273,7 +287,7 @@ void ModelEngineBuilder::analyzeModel( FirstOrderModel* fm ){ } } //for calculating terms that we don't need to consider - if( !n.getAttribute(NoMatchAttribute()) || n.getAttribute(ModelBasisArgAttribute())==1 ){ + if( !n.getAttribute(NoMatchAttribute()) || n.getAttribute(ModelBasisArgAttribute())!=0 ){ if( !n.getAttribute(BasisNoMatchAttribute()) ){ //need to consider if it is not congruent modulo model basis if( !tabt.addTerm( fm, n ) ){ @@ -296,7 +310,7 @@ void ModelEngineBuilder::analyzeModel( FirstOrderModel* fm ){ } } -bool ModelEngineBuilder::hasConstantDefinition( Node n ){ +bool QModelBuilderIG::hasConstantDefinition( Node n ){ Node lit = n.getKind()==NOT ? n[0] : n; if( lit.getKind()==APPLY_UF ){ Node op = lit.getOperator(); @@ -307,31 +321,19 @@ bool ModelEngineBuilder::hasConstantDefinition( Node n ){ return false; } -bool ModelEngineBuilder::optUseModel() { - return options::fmfModelBasedInst(); -} - -bool ModelEngineBuilder::optInstGen(){ +bool QModelBuilderIG::optInstGen(){ return options::fmfInstGen(); } -bool ModelEngineBuilder::optOneQuantPerRoundInstGen(){ +bool QModelBuilderIG::optOneQuantPerRoundInstGen(){ return options::fmfInstGenOneQuantPerRound(); } -bool ModelEngineBuilder::optExhInstNonInstGenQuant(){ - return options::fmfNewInstGen(); -} - -void ModelEngineBuilder::setEffort( int effort ){ - d_considerAxioms = effort>=1; -} - -ModelEngineBuilder::Statistics::Statistics(): - d_num_quants_init("ModelEngineBuilder::Number_Quantifiers", 0), - d_num_partial_quants_init("ModelEngineBuilder::Number_Partial_Quantifiers", 0), - d_init_inst_gen_lemmas("ModelEngineBuilder::Initialize_Inst_Gen_Lemmas", 0 ), - d_inst_gen_lemmas("ModelEngineBuilder::Inst_Gen_Lemmas", 0 ) +QModelBuilderIG::Statistics::Statistics(): + d_num_quants_init("QModelBuilder::Number_Quantifiers", 0), + d_num_partial_quants_init("QModelBuilder::Number_Partial_Quantifiers", 0), + d_init_inst_gen_lemmas("QModelBuilder::Initialize_Inst_Gen_Lemmas", 0 ), + d_inst_gen_lemmas("QModelBuilder::Inst_Gen_Lemmas", 0 ) { StatisticsRegistry::registerStat(&d_num_quants_init); StatisticsRegistry::registerStat(&d_num_partial_quants_init); @@ -339,20 +341,20 @@ ModelEngineBuilder::Statistics::Statistics(): StatisticsRegistry::registerStat(&d_inst_gen_lemmas); } -ModelEngineBuilder::Statistics::~Statistics(){ +QModelBuilderIG::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_num_quants_init); StatisticsRegistry::unregisterStat(&d_num_partial_quants_init); StatisticsRegistry::unregisterStat(&d_init_inst_gen_lemmas); StatisticsRegistry::unregisterStat(&d_inst_gen_lemmas); } -bool ModelEngineBuilder::isQuantifierActive( Node f ){ +bool QModelBuilderIG::isQuantifierActive( Node f ){ return ( d_considerAxioms || !f.getAttribute(AxiomAttribute()) ) && d_quant_sat.find( f )==d_quant_sat.end(); } -bool ModelEngineBuilder::isTermActive( Node n ){ +bool QModelBuilderIG::isTermActive( Node n ){ return !n.getAttribute(NoMatchAttribute()) || //it is not congruent to another active term - ( n.getAttribute(ModelBasisArgAttribute())==1 && !n.getAttribute(BasisNoMatchAttribute()) ); //or it has model basis arguments + ( n.getAttribute(ModelBasisArgAttribute())!=0 && !n.getAttribute(BasisNoMatchAttribute()) ); //or it has model basis arguments //and is not congruent modulo model basis //to another active term } @@ -360,7 +362,7 @@ bool ModelEngineBuilder::isTermActive( Node n ){ -void ModelEngineBuilderDefault::reset( FirstOrderModel* fm ){ +void QModelBuilderDefault::reset( FirstOrderModel* fm ){ d_quant_selection_lit.clear(); d_quant_selection_lit_candidates.clear(); d_quant_selection_lit_terms.clear(); @@ -369,7 +371,7 @@ void ModelEngineBuilderDefault::reset( FirstOrderModel* fm ){ } -int ModelEngineBuilderDefault::getSelectionScore( std::vector< Node >& uf_terms ) { +int QModelBuilderDefault::getSelectionScore( std::vector< Node >& uf_terms ) { /* size_t maxChildren = 0; for( size_t i=0; i<uf_terms.size(); i++ ){ @@ -383,7 +385,7 @@ int ModelEngineBuilderDefault::getSelectionScore( std::vector< Node >& uf_terms return 0; } -void ModelEngineBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ){ +void QModelBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ){ Debug("fmf-model-prefs") << "Analyze quantifier " << f << std::endl; //the pro/con preferences for this quantifier std::vector< Node > pro_con[2]; @@ -513,7 +515,7 @@ void ModelEngineBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ) } } -int ModelEngineBuilderDefault::doInstGen( FirstOrderModel* fm, Node f ){ +int QModelBuilderDefault::doInstGen( FirstOrderModel* fm, Node f ){ int addedLemmas = 0; //we wish to add all known exceptions to our selection literal for f. this will help to refine our current model. //This step is advantageous over exhaustive instantiation, since we are adding instantiations that involve model basis terms, @@ -564,7 +566,7 @@ int ModelEngineBuilderDefault::doInstGen( FirstOrderModel* fm, Node f ){ return addedLemmas; } -void ModelEngineBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ){ +void QModelBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ){ if( optReconsiderFuncConstants() ){ //reconsider constant functions that weren't necessary if( d_uf_model_constructed[op] ){ @@ -597,7 +599,7 @@ void ModelEngineBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ) fm->d_uf_model_gen[op].setValue( fm, n, v ); if( fm->d_uf_model_gen[op].optUsePartialDefaults() ){ //also set as default value if necessary - if( n.hasAttribute(ModelBasisArgAttribute()) && n.getAttribute(ModelBasisArgAttribute())==1 ){ + if( n.hasAttribute(ModelBasisArgAttribute()) && n.getAttribute(ModelBasisArgAttribute())!=0 ){ Trace("fmf-model-cons") << " Set as default." << std::endl; fm->d_uf_model_gen[op].setValue( fm, n, v, false ); if( n==defaultTerm ){ @@ -619,6 +621,13 @@ void ModelEngineBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ) Trace("fmf-model-cons") << " Choose default value..." << std::endl; //chose defaultVal based on heuristic, currently the best ratio of "pro" responses Node defaultVal = d_uf_prefs[op].getBestDefaultValue( defaultTerm, fm ); + if( defaultVal.isNull() ){ + if (!fm->d_rep_set.hasType(defaultTerm.getType())) { + Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(defaultTerm.getType()); + fm->d_rep_set.d_type_reps[defaultTerm.getType()].push_back(mbt); + } + defaultVal = fm->d_rep_set.d_type_reps[defaultTerm.getType()][0]; + } Assert( !defaultVal.isNull() ); Trace("fmf-model-cons") << "Set default term : " << fm->d_rep_set.getIndexFor( defaultVal ) << std::endl; fm->d_uf_model_gen[op].setValue( fm, defaultTerm, defaultVal, false ); @@ -635,7 +644,7 @@ void ModelEngineBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ) ////////////////////// Inst-Gen style Model Builder /////////// -void ModelEngineBuilderInstGen::reset( FirstOrderModel* fm ){ +void QModelBuilderInstGen::reset( FirstOrderModel* fm ){ //for new inst gen d_quant_selection_formula.clear(); d_term_selected.clear(); @@ -643,15 +652,15 @@ void ModelEngineBuilderInstGen::reset( FirstOrderModel* fm ){ //d_sub_quant_inst_trie.clear();//* } -int ModelEngineBuilderInstGen::initializeQuantifier( Node f, Node fp ){ - int addedLemmas = ModelEngineBuilder::initializeQuantifier( f, fp ); +int QModelBuilderInstGen::initializeQuantifier( Node f, Node fp ){ + int addedLemmas = QModelBuilderIG::initializeQuantifier( f, fp ); for( size_t i=0; i<d_sub_quants[f].size(); i++ ){ addedLemmas += initializeQuantifier( d_sub_quants[f][i], fp ); } return addedLemmas; } -void ModelEngineBuilderInstGen::analyzeQuantifier( FirstOrderModel* fm, Node f ){ +void QModelBuilderInstGen::analyzeQuantifier( FirstOrderModel* fm, Node f ){ //Node fp = getParentQuantifier( f );//* //bool quantRedundant = ( f!=fp && d_sub_quant_inst_trie[fp].addInstMatch( d_qe, fp, d_sub_quant_inst[ f ], true ) ); //if( f==fp || d_sub_quant_inst_trie[fp].addInstMatch( d_qe, fp, d_sub_quant_inst[ f ], true ) ){//* @@ -685,7 +694,7 @@ void ModelEngineBuilderInstGen::analyzeQuantifier( FirstOrderModel* fm, Node f ) } -int ModelEngineBuilderInstGen::doInstGen( FirstOrderModel* fm, Node f ){ +int QModelBuilderInstGen::doInstGen( FirstOrderModel* fm, Node f ){ int addedLemmas = 0; if( d_quant_sat.find( f )==d_quant_sat.end() ){ Node fp = d_sub_quant_parent.find( f )==d_sub_quant_parent.end() ? f : d_sub_quant_parent[f]; @@ -802,7 +811,7 @@ Node mkAndSelectionFormula( Node n1, Node n2 ){ //if possible, returns a formula n' such that n' => ( n <=> polarity ), and n' is true in the current context, // and NULL otherwise -Node ModelEngineBuilderInstGen::getSelectionFormula( Node fn, Node n, bool polarity, int useOption ){ +Node QModelBuilderInstGen::getSelectionFormula( Node fn, Node n, bool polarity, int useOption ){ Trace("sel-form-debug") << "Looking for selection formula " << n << " " << polarity << std::endl; Node ret; if( n.getKind()==NOT ){ @@ -911,7 +920,7 @@ Node ModelEngineBuilderInstGen::getSelectionFormula( Node fn, Node n, bool polar return ret; } -int ModelEngineBuilderInstGen::getSelectionFormulaScore( Node fn ){ +int QModelBuilderInstGen::getSelectionFormulaScore( Node fn ){ if( fn.getType().isBoolean() ){ if( fn.getKind()==APPLY_UF ){ Node op = fn.getOperator(); @@ -929,13 +938,13 @@ int ModelEngineBuilderInstGen::getSelectionFormulaScore( Node fn ){ } } -void ModelEngineBuilderInstGen::setSelectedTerms( Node s ){ +void QModelBuilderInstGen::setSelectedTerms( Node s ){ //if it is apply uf and has model basis arguments, then mark term as being "selected" if( s.getKind()==APPLY_UF ){ Assert( s.hasAttribute(ModelBasisArgAttribute()) ); if( !s.hasAttribute(ModelBasisArgAttribute()) ) std::cout << "no mba!! " << s << std::endl; - if( s.getAttribute(ModelBasisArgAttribute())==1 ){ + if( s.getAttribute(ModelBasisArgAttribute())!=0 ){ d_term_selected[ s ] = true; Trace("sel-form-term") << " " << s << " is a selected term." << std::endl; } @@ -945,7 +954,7 @@ void ModelEngineBuilderInstGen::setSelectedTerms( Node s ){ } } -bool ModelEngineBuilderInstGen::isUsableSelectionLiteral( Node n, int useOption ){ +bool QModelBuilderInstGen::isUsableSelectionLiteral( Node n, int useOption ){ if( n.getKind()==FORALL ){ return false; }else if( n.getKind()!=APPLY_UF ){ @@ -964,7 +973,7 @@ bool ModelEngineBuilderInstGen::isUsableSelectionLiteral( Node n, int useOption return true; } -void ModelEngineBuilderInstGen::getParentQuantifierMatch( InstMatch& mp, Node fp, InstMatch& m, Node f ){ +void QModelBuilderInstGen::getParentQuantifierMatch( InstMatch& mp, Node fp, InstMatch& m, Node f ){ if( f!=fp ){ //std::cout << "gpqm " << fp << " " << f << " " << m << std::endl; //std::cout << " " << fp[0].getNumChildren() << " " << f[0].getNumChildren() << std::endl; @@ -988,7 +997,7 @@ void ModelEngineBuilderInstGen::getParentQuantifierMatch( InstMatch& mp, Node fp } } -void ModelEngineBuilderInstGen::constructModelUf( FirstOrderModel* fm, Node op ){ +void QModelBuilderInstGen::constructModelUf( FirstOrderModel* fm, Node op ){ bool setDefaultVal = true; Node defaultTerm = d_qe->getTermDatabase()->getModelBasisOpTerm( op ); //set the values in the model @@ -1016,6 +1025,6 @@ void ModelEngineBuilderInstGen::constructModelUf( FirstOrderModel* fm, Node op ) d_uf_model_constructed[op] = true; } -bool ModelEngineBuilderInstGen::existsInstantiation( Node f, InstMatch& m, bool modEq, bool modInst ){ +bool QModelBuilderInstGen::existsInstantiation( Node f, InstMatch& m, bool modEq, bool modInst ){ return d_child_sub_quant_inst_trie[f].existsInstMatch( d_qe, f, m, modEq, true ); }
\ No newline at end of file diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h index 31448acee..2b38f3381 100644 --- a/src/theory/quantifiers/model_builder.h +++ b/src/theory/quantifiers/model_builder.h @@ -25,6 +25,35 @@ namespace CVC4 { namespace theory { namespace quantifiers { + +class QModelBuilder : public TheoryEngineModelBuilder +{ +protected: + //the model we are working with + context::CDO< FirstOrderModel* > d_curr_model; + //quantifiers engine + QuantifiersEngine* d_qe; +public: + QModelBuilder( context::Context* c, QuantifiersEngine* qe ); + virtual ~QModelBuilder(){} + // is quantifier active? + virtual bool isQuantifierActive( Node f ) { return true; } + //do exhaustive instantiation + virtual bool doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort, int & lemmas ) { return false; } + //whether to construct model + virtual bool optUseModel(); + /** number of lemmas generated while building model */ + int d_addedLemmas; + //consider axioms + bool d_considerAxioms; + /** exist instantiation ? */ + virtual bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false ) { return false; } +}; + + + + + /** Attribute true for nodes that should not be used when considered for inst-gen basis */ struct BasisNoMatchAttributeId {}; /** use the special for boolean flag */ @@ -47,17 +76,13 @@ public: /** model builder class * This class is capable of building candidate models based on the current quantified formulas * that are asserted. Use: - * (1) call ModelEngineBuilder::buildModel( m, false );, where m is a FirstOrderModel + * (1) call QModelBuilder::buildModel( m, false );, where m is a FirstOrderModel * (2) if candidate model is determined to be a real model, - then call ModelEngineBuilder::buildModel( m, true ); + then call QModelBuilder::buildModel( m, true ); */ -class ModelEngineBuilder : public TheoryEngineModelBuilder +class QModelBuilderIG : public QModelBuilder { protected: - //quantifiers engine - QuantifiersEngine* d_qe; - //the model we are working with - context::CDO< FirstOrderModel* > d_curr_model; //map from operators to model preference data std::map< Node, uf::UfModelPreferenceData > d_uf_prefs; //built model uf @@ -90,25 +115,15 @@ protected: //helper functions /** term has constant definition */ bool hasConstantDefinition( Node n ); public: - ModelEngineBuilder( context::Context* c, QuantifiersEngine* qe ); - virtual ~ModelEngineBuilder(){} - /** number of lemmas generated while building model */ - int d_addedLemmas; - //consider axioms - bool d_considerAxioms; - // set effort - void setEffort( int effort ); + QModelBuilderIG( context::Context* c, QuantifiersEngine* qe ); + virtual ~QModelBuilderIG(){} //debug model void debugModel( FirstOrderModel* fm ); public: - //whether to construct model - virtual bool optUseModel(); //whether to add inst-gen lemmas virtual bool optInstGen(); //whether to only consider only quantifier per round of inst-gen virtual bool optOneQuantPerRoundInstGen(); - //whether we should exhaustively instantiate quantifiers where inst-gen is not working - virtual bool optExhInstNonInstGenQuant(); /** statistics class */ class Statistics { public: @@ -120,18 +135,16 @@ public: ~Statistics(); }; Statistics d_statistics; - // is quantifier active? - bool isQuantifierActive( Node f ); // is term active bool isTermActive( Node n ); // is term selected virtual bool isTermSelected( Node n ) { return false; } - /** exist instantiation ? */ - virtual bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false ) { return false; } /** quantifier has inst-gen definition */ virtual bool hasInstGen( Node f ) = 0; /** did inst gen this round? */ bool didInstGen() { return d_didInstGen; } + // is quantifier active? + bool isQuantifierActive( Node f ); //temporary stats int d_numQuantSat; @@ -140,10 +153,10 @@ public: int d_numQuantNoSelForm; //temporary stat int d_instGenMatches; -};/* class ModelEngineBuilder */ +};/* class QModelBuilder */ -class ModelEngineBuilderDefault : public ModelEngineBuilder +class QModelBuilderDefault : public QModelBuilderIG { private: ///information for (old) InstGen //map from quantifiers to their selection literals @@ -167,15 +180,15 @@ protected: //theory-specific build models void constructModelUf( FirstOrderModel* fm, Node op ); public: - ModelEngineBuilderDefault( context::Context* c, QuantifiersEngine* qe ) : ModelEngineBuilder( c, qe ){} - ~ModelEngineBuilderDefault(){} + QModelBuilderDefault( context::Context* c, QuantifiersEngine* qe ) : QModelBuilderIG( c, qe ){} + ~QModelBuilderDefault(){} //options bool optReconsiderFuncConstants() { return true; } //has inst gen bool hasInstGen( Node f ) { return !d_quant_selection_lit[f].isNull(); } }; -class ModelEngineBuilderInstGen : public ModelEngineBuilder +class QModelBuilderInstGen : public QModelBuilderIG { private: ///information for (new) InstGen //map from quantifiers to their selection formulas @@ -217,8 +230,8 @@ private: //get parent quantifier Node getParentQuantifier( Node f ) { return d_sub_quant_parent.find( f )==d_sub_quant_parent.end() ? f : d_sub_quant_parent[f]; } public: - ModelEngineBuilderInstGen( context::Context* c, QuantifiersEngine* qe ) : ModelEngineBuilder( c, qe ){} - ~ModelEngineBuilderInstGen(){} + QModelBuilderInstGen( context::Context* c, QuantifiersEngine* qe ) : QModelBuilderIG( c, qe ){} + ~QModelBuilderInstGen(){} // is term selected bool isTermSelected( Node n ) { return d_term_selected.find( n )!=d_term_selected.end(); } /** exist instantiation ? */ diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index a69b278c0..b9dcef282 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -38,10 +38,12 @@ ModelEngine::ModelEngine( context::Context* c, QuantifiersEngine* qe ) : QuantifiersModule( qe ), d_rel_domain( qe, qe->getModel() ){ - if( options::fmfNewInstGen() ){ - d_builder = new ModelEngineBuilderInstGen( c, qe ); + if( options::fmfFullModelCheck() ){ + d_builder = new fmcheck::FullModelChecker( c, qe ); + }else if( options::fmfNewInstGen() ){ + d_builder = new QModelBuilderInstGen( c, qe ); }else{ - d_builder = new ModelEngineBuilderDefault( c, qe ); + d_builder = new QModelBuilderDefault( c, qe ); } } @@ -66,7 +68,7 @@ void ModelEngine::check( Theory::Effort e ){ Trace("model-engine") << "---Model Engine Round---" << std::endl; //initialize the model Trace("model-engine-debug") << "Build model..." << std::endl; - d_builder->setEffort( effort ); + d_builder->d_considerAxioms = effort>=1; d_builder->buildModel( fm, false ); addedLemmas += (int)d_builder->d_addedLemmas; //if builder has lemmas, add and return @@ -81,11 +83,7 @@ void ModelEngine::check( Theory::Effort e ){ Debug("fmf-model-complete") << std::endl; debugPrint("fmf-model-complete"); //successfully built an acceptable model, now check it - addedLemmas += checkModel( check_model_full ); - }else if( d_builder->didInstGen() && d_builder->optExhInstNonInstGenQuant() ){ - Trace("model-engine-debug") << "Check model for non-inst gen quantifiers..." << std::endl; - //check quantifiers that inst-gen didn't apply to - addedLemmas += checkModel( check_model_no_inst_gen ); + addedLemmas += checkModel(); } } if( addedLemmas==0 ){ @@ -151,7 +149,7 @@ bool ModelEngine::optExhInstEvalSkipMultiple(){ #endif } -int ModelEngine::checkModel( int checkOption ){ +int ModelEngine::checkModel(){ int addedLemmas = 0; FirstOrderModel* fm = d_quantEngine->getModel(); //for debugging @@ -161,15 +159,25 @@ int ModelEngine::checkModel( int checkOption ){ if( it->first.isSort() ){ Trace("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl; Trace("model-engine-debug") << " "; + Node mbt = d_quantEngine->getTermDatabase()->getModelBasisTerm(it->first); for( size_t i=0; i<it->second.size(); i++ ){ //Trace("model-engine-debug") << it->second[i] << " "; Node r = ((EqualityQueryQuantifiersEngine*)d_quantEngine->getEqualityQuery())->getRepresentative( it->second[i] ); Trace("model-engine-debug") << r << " "; } Trace("model-engine-debug") << std::endl; + Trace("model-engine-debug") << " Model basis term : " << mbt << std::endl; } } } + //full model checking: construct models for all functions + /* + if( d_fmc.isActive() ){ + for (std::map< Node, uf::UfModelTreeGenerator >::iterator it = fm->d_uf_model_gen.begin(); it != fm->d_uf_model_gen.end(); ++it) { + d_fmc.getModel(fm, it->first); + } + } + */ //compute the relevant domain if necessary if( optUseRelevantDomain() ){ d_rel_domain.compute(); @@ -179,36 +187,34 @@ int ModelEngine::checkModel( int checkOption ){ d_relevantLemmas = 0; d_totalLemmas = 0; Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl; - for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ - Node f = fm->getAssertedQuantifier( i ); - //keep track of total instantiations for statistics - int totalInst = 1; - for( size_t i=0; i<f[0].getNumChildren(); i++ ){ - TypeNode tn = f[0][i].getType(); - if( fm->d_rep_set.hasType( tn ) ){ - totalInst = totalInst * (int)fm->d_rep_set.d_type_reps[ tn ].size(); - } - } - d_totalLemmas += totalInst; - //determine if we should check this quantifiers - bool checkQuant = false; - if( checkOption==check_model_full ){ - checkQuant = d_builder->isQuantifierActive( f ); - }else if( checkOption==check_model_no_inst_gen ){ - checkQuant = !d_builder->hasInstGen( f ); - } - //if we need to consider this quantifier on this iteration - if( checkQuant ){ - addedLemmas += exhaustiveInstantiate( f, optUseRelevantDomain() ); - if( Trace.isOn("model-engine-warn") ){ - if( addedLemmas>10000 ){ - Debug("fmf-exit") << std::endl; - debugPrint("fmf-exit"); - exit( 0 ); + int e_max = options::fmfFullModelCheck() ? 2 : 1; + for( int e=0; e<e_max; e++) { + if (addedLemmas==0) { + for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ + Node f = fm->getAssertedQuantifier( i ); + //keep track of total instantiations for statistics + int totalInst = 1; + for( size_t i=0; i<f[0].getNumChildren(); i++ ){ + TypeNode tn = f[0][i].getType(); + if( fm->d_rep_set.hasType( tn ) ){ + totalInst = totalInst * (int)fm->d_rep_set.d_type_reps[ tn ].size(); + } + } + d_totalLemmas += totalInst; + //determine if we should check this quantifier + if( d_builder->isQuantifierActive( f ) ){ + addedLemmas += exhaustiveInstantiate( f, e ); + if( Trace.isOn("model-engine-warn") ){ + if( addedLemmas>10000 ){ + Debug("fmf-exit") << std::endl; + debugPrint("fmf-exit"); + exit( 0 ); + } + } + if( optOneQuantPerRound() && addedLemmas>0 ){ + break; + } } - } - if( optOneQuantPerRound() && addedLemmas>0 ){ - break; } } } @@ -222,100 +228,102 @@ int ModelEngine::checkModel( int checkOption ){ return addedLemmas; } -int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain ){ +int ModelEngine::exhaustiveInstantiate( Node f, int effort ){ int addedLemmas = 0; - Trace("inst-fmf-ei") << "Exhaustive instantiate " << f << "..." << std::endl; - Debug("inst-fmf-ei") << " Instantiation Constants: "; - for( size_t i=0; i<f[0].getNumChildren(); i++ ){ - Debug("inst-fmf-ei") << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) << " "; - } - Debug("inst-fmf-ei") << std::endl; - - //create a rep set iterator and iterate over the (relevant) domain of the quantifier - RepSetIterator riter( &(d_quantEngine->getModel()->d_rep_set) ); - if( riter.setQuantifier( f ) ){ - //set the domain for the iterator (the sufficient set of instantiations to try) - if( useRelInstDomain ){ - riter.setDomain( d_rel_domain.d_quant_inst_domain[f] ); + if( !d_builder->doExhaustiveInstantiation( d_quantEngine->getModel(), f, effort, addedLemmas ) ){ + Trace("inst-fmf-ei") << "Exhaustive instantiate " << f << ", effort = " << effort << "..." << std::endl; + Debug("inst-fmf-ei") << " Instantiation Constants: "; + for( size_t i=0; i<f[0].getNumChildren(); i++ ){ + Debug("inst-fmf-ei") << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) << " "; } - d_quantEngine->getModel()->resetEvaluate(); - int tests = 0; - int triedLemmas = 0; - while( !riter.isFinished() && ( addedLemmas==0 || !optOneInstPerQuantRound() ) ){ - d_testLemmas++; - int eval = 0; - int depIndex; - if( d_builder->optUseModel() ){ - //see if instantiation is already true in current model - Debug("fmf-model-eval") << "Evaluating "; - riter.debugPrintSmall("fmf-model-eval"); - Debug("fmf-model-eval") << "Done calculating terms." << std::endl; - tests++; - //if evaluate(...)==1, then the instantiation is already true in the model - // depIndex is the index of the least significant variable that this evaluation relies upon - depIndex = riter.getNumTerms()-1; - eval = d_quantEngine->getModel()->evaluate( d_quantEngine->getTermDatabase()->getInstConstantBody( f ), depIndex, &riter ); - if( eval==1 ){ - Debug("fmf-model-eval") << " Returned success with depIndex = " << depIndex << std::endl; - }else{ - Debug("fmf-model-eval") << " Returned " << (eval==-1 ? "failure" : "unknown") << ", depIndex = " << depIndex << std::endl; + Debug("inst-fmf-ei") << std::endl; + //create a rep set iterator and iterate over the (relevant) domain of the quantifier + RepSetIterator riter( &(d_quantEngine->getModel()->d_rep_set) ); + if( riter.setQuantifier( d_quantEngine, f ) ){ + Debug("inst-fmf-ei") << "Reset evaluate..." << std::endl; + d_quantEngine->getModel()->resetEvaluate(); + Debug("inst-fmf-ei") << "Begin instantiation..." << std::endl; + int tests = 0; + int triedLemmas = 0; + while( !riter.isFinished() && ( addedLemmas==0 || !optOneInstPerQuantRound() ) ){ + for( int i=0; i<(int)riter.d_index.size(); i++ ){ + Trace("try") << i << " : " << riter.d_index[i] << " : " << riter.getTerm( i ) << std::endl; } - } - if( eval==1 ){ - //instantiation is already true -> skip - riter.increment2( depIndex ); - }else{ - //instantiation was not shown to be true, construct the match - InstMatch m; - for( int i=0; i<riter.getNumTerms(); i++ ){ - m.set( d_quantEngine->getTermDatabase()->getInstantiationConstant( f, riter.d_index_order[i] ), riter.getTerm( i ) ); + d_testLemmas++; + int eval = 0; + int depIndex; + if( d_builder->optUseModel() ){ + //see if instantiation is already true in current model + Debug("fmf-model-eval") << "Evaluating "; + riter.debugPrintSmall("fmf-model-eval"); + Debug("fmf-model-eval") << "Done calculating terms." << std::endl; + tests++; + //if evaluate(...)==1, then the instantiation is already true in the model + // depIndex is the index of the least significant variable that this evaluation relies upon + depIndex = riter.getNumTerms()-1; + eval = d_quantEngine->getModel()->evaluate( d_quantEngine->getTermDatabase()->getInstConstantBody( f ), depIndex, &riter ); + if( eval==1 ){ + Debug("fmf-model-eval") << " Returned success with depIndex = " << depIndex << std::endl; + }else{ + Debug("fmf-model-eval") << " Returned " << (eval==-1 ? "failure" : "unknown") << ", depIndex = " << depIndex << std::endl; + } } - Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl; - triedLemmas++; - d_triedLemmas++; - //add as instantiation - if( d_quantEngine->addInstantiation( f, m ) ){ - addedLemmas++; - //if the instantiation is show to be false, and we wish to skip multiple instantiations at once - if( eval==-1 && optExhInstEvalSkipMultiple() ){ - riter.increment2( depIndex ); + if( eval==1 ){ + //instantiation is already true -> skip + riter.increment2( depIndex ); + }else{ + //instantiation was not shown to be true, construct the match + InstMatch m; + for( int i=0; i<riter.getNumTerms(); i++ ){ + m.set( d_quantEngine, f, riter.d_index_order[i], riter.getTerm( i ) ); + } + Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl; + triedLemmas++; + d_triedLemmas++; + //add as instantiation + if( d_quantEngine->addInstantiation( f, m ) ){ + addedLemmas++; + //if the instantiation is show to be false, and we wish to skip multiple instantiations at once + if( eval==-1 && optExhInstEvalSkipMultiple() ){ + riter.increment2( depIndex ); + }else{ + riter.increment(); + } }else{ + Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl; riter.increment(); } - }else{ - Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl; - riter.increment(); } } + //print debugging information + d_statistics.d_eval_formulas += d_quantEngine->getModel()->d_eval_formulas; + d_statistics.d_eval_uf_terms += d_quantEngine->getModel()->d_eval_uf_terms; + d_statistics.d_eval_lits += d_quantEngine->getModel()->d_eval_lits; + d_statistics.d_eval_lits_unknown += d_quantEngine->getModel()->d_eval_lits_unknown; + int relevantInst = 1; + for( size_t i=0; i<f[0].getNumChildren(); i++ ){ + relevantInst = relevantInst * (int)riter.d_domain[i].size(); + } + d_relevantLemmas += relevantInst; + Trace("inst-fmf-ei") << "Finished: " << std::endl; + //Debug("inst-fmf-ei") << " Inst Total: " << totalInst << std::endl; + Trace("inst-fmf-ei") << " Inst Relevant: " << relevantInst << std::endl; + Trace("inst-fmf-ei") << " Inst Tried: " << triedLemmas << std::endl; + Trace("inst-fmf-ei") << " Inst Added: " << addedLemmas << std::endl; + Trace("inst-fmf-ei") << " # Tests: " << tests << std::endl; + if( addedLemmas>1000 ){ + Trace("model-engine-warn") << "WARNING: many instantiations produced for " << f << ": " << std::endl; + //Trace("model-engine-warn") << " Inst Total: " << totalInst << std::endl; + Trace("model-engine-warn") << " Inst Relevant: " << relevantInst << std::endl; + Trace("model-engine-warn") << " Inst Tried: " << triedLemmas << std::endl; + Trace("model-engine-warn") << " Inst Added: " << addedLemmas << std::endl; + Trace("model-engine-warn") << " # Tests: " << tests << std::endl; + Trace("model-engine-warn") << std::endl; + } } - //print debugging information - d_statistics.d_eval_formulas += d_quantEngine->getModel()->d_eval_formulas; - d_statistics.d_eval_uf_terms += d_quantEngine->getModel()->d_eval_uf_terms; - d_statistics.d_eval_lits += d_quantEngine->getModel()->d_eval_lits; - d_statistics.d_eval_lits_unknown += d_quantEngine->getModel()->d_eval_lits_unknown; - int relevantInst = 1; - for( size_t i=0; i<f[0].getNumChildren(); i++ ){ - relevantInst = relevantInst * (int)riter.d_domain[i].size(); - } - d_relevantLemmas += relevantInst; - Trace("inst-fmf-ei") << "Finished: " << std::endl; - //Debug("inst-fmf-ei") << " Inst Total: " << totalInst << std::endl; - Trace("inst-fmf-ei") << " Inst Relevant: " << relevantInst << std::endl; - Trace("inst-fmf-ei") << " Inst Tried: " << triedLemmas << std::endl; - Trace("inst-fmf-ei") << " Inst Added: " << addedLemmas << std::endl; - Trace("inst-fmf-ei") << " # Tests: " << tests << std::endl; - if( addedLemmas>1000 ){ - Trace("model-engine-warn") << "WARNING: many instantiations produced for " << f << ": " << std::endl; - //Trace("model-engine-warn") << " Inst Total: " << totalInst << std::endl; - Trace("model-engine-warn") << " Inst Relevant: " << relevantInst << std::endl; - Trace("model-engine-warn") << " Inst Tried: " << triedLemmas << std::endl; - Trace("model-engine-warn") << " Inst Added: " << addedLemmas << std::endl; - Trace("model-engine-warn") << " # Tests: " << tests << std::endl; - Trace("model-engine-warn") << std::endl; - } + //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round + d_incomplete_check = d_incomplete_check || riter.d_incomplete; } - //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round - d_incomplete_check = d_incomplete_check || riter.d_incomplete; return addedLemmas; } diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h index 386864164..97aa085ed 100644 --- a/src/theory/quantifiers/model_engine.h +++ b/src/theory/quantifiers/model_engine.h @@ -21,6 +21,7 @@ #include "theory/quantifiers/model_builder.h" #include "theory/model.h" #include "theory/quantifiers/relevant_domain.h" +#include "theory/quantifiers/full_model_check.h" namespace CVC4 { namespace theory { @@ -31,7 +32,7 @@ class ModelEngine : public QuantifiersModule friend class RepSetIterator; private: /** builder class */ - ModelEngineBuilder* d_builder; + QModelBuilder* d_builder; private: //analysis of current model: //relevant domain RelevantDomain d_rel_domain; @@ -44,14 +45,10 @@ private: bool optOneQuantPerRound(); bool optExhInstEvalSkipMultiple(); private: - enum{ - check_model_full, - check_model_no_inst_gen, - }; //check model - int checkModel( int checkOption ); + int checkModel(); //exhaustively instantiate quantifier (possibly using mbqi), return number of lemmas produced - int exhaustiveInstantiate( Node f, bool useRelInstDomain = false ); + int exhaustiveInstantiate( Node f, int effort = 0 ); private: //temporary statistics int d_triedLemmas; @@ -62,7 +59,7 @@ public: ModelEngine( context::Context* c, QuantifiersEngine* qe ); ~ModelEngine(){} //get the builder - ModelEngineBuilder* getModelBuilder() { return d_builder; } + QModelBuilder* getModelBuilder() { return d_builder; } public: void check( Theory::Effort e ); void registerQuantifier( Node f ); diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 60f5a171d..9facdbc5f 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -47,6 +47,9 @@ option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false # Whether to perform quantifier macro expansion option macrosQuant --macros-quant bool :default false perform quantifiers macro expansions +# Whether to perform first-order propagation +option foPropQuant --fo-prop-quant bool :default false + perform first-order propagation on quantifiers # Whether to use smart triggers option smartTriggers /--disable-smart-triggers bool :default true @@ -54,6 +57,8 @@ option smartTriggers /--disable-smart-triggers bool :default true # Whether to use relevent triggers option relevantTriggers /--disable-relevant-triggers bool :default true prefer triggers that are more relevant based on SInE style analysis +option relationalTriggers --relational-triggers bool :default false + choose relational triggers such as x = f(y), x >= f(y) # Whether to consider terms in the bodies of quantifiers for matching option registerQuantBodyTerms --register-quant-body-terms bool :default false @@ -88,6 +93,11 @@ option finiteModelFind --finite-model-find bool :default false option fmfModelBasedInst /--disable-fmf-mbqi bool :default true disable model-based quantifier instantiation for finite model finding +option fmfFullModelCheck --fmf-fmc bool :default false + enable full model check for finite model finding +option fmfFullModelCheckSimple /--disable-fmf-fmc-simple bool :default true + disable simple models in full model check for finite model finding + option fmfOneInstPerRound --fmf-one-inst-per-round bool :default false only add one instantiation per quantifier per round for fmf option fmfOneQuantPerRound --fmf-one-quant-per-round bool :default false @@ -98,8 +108,9 @@ option fmfRelevantDomain --fmf-relevant-domain bool :default false use relevant domain computation, similar to complete instantiation (Ge, deMoura 09) option fmfNewInstGen --fmf-new-inst-gen bool :default false use new inst gen technique for answering sat without exhaustive instantiation -option fmfInstGen /--disable-fmf-inst-gen bool :default true - disable Inst-Gen instantiation techniques for finite model finding +option fmfInstGen --fmf-inst-gen/--disable-fmf-inst-gen bool :read-write :default true + enable Inst-Gen instantiation techniques for finite model finding (default) +/disable Inst-Gen instantiation techniques for finite model finding option fmfInstGenOneQuantPerRound --fmf-inst-gen-one-quant-per-round bool :default false only perform Inst-Gen instantiation techniques on one quantifier per round option fmfFreshDistConst --fmf-fresh-dc bool :default false diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index 36db56d0d..53f67853b 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -22,6 +22,102 @@ using namespace CVC4::kind; using namespace CVC4::context; using namespace CVC4::theory; + +bool QuantArith::getMonomial( Node n, std::map< Node, Node >& msum ) { + if ( n.getKind()==MULT ){ + if( n.getNumChildren()==2 && msum.find(n[1])==msum.end() && n[0].isConst() ){ + msum[n[1]] = n[0]; + return true; + } + }else{ + if( msum.find(n)==msum.end() ){ + msum[n] = Node::null(); + return true; + } + } + return false; +} + +bool QuantArith::getMonomialSum( Node n, std::map< Node, Node >& msum ) { + if ( n.getKind()==PLUS ){ + for( unsigned i=0; i<n.getNumChildren(); i++) { + if (!getMonomial( n[i], msum )){ + return false; + } + } + return true; + }else{ + return getMonomial( n, msum ); + } +} + +bool QuantArith::getMonomialSumLit( Node lit, std::map< Node, Node >& msum ) { + if( lit.getKind()==GEQ || lit.getKind()==EQUAL ){ + if( getMonomialSum( lit[0], msum ) ){ + if( lit[1].isConst() ){ + if( !lit[1].getConst<Rational>().isZero() ){ + msum[Node::null()] = negate( lit[1] ); + } + return true; + } + } + } + return false; +} + +bool QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind k ) { + if( msum.find(v)!=msum.end() ){ + std::vector< Node > children; + Rational r = msum[v].isNull() ? Rational(1) : msum[v].getConst<Rational>(); + if ( r.sgn()!=0 ){ + for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ + if( it->first.isNull() || it->first!=v ){ + Node m; + if( !it->first.isNull() ){ + if ( !it->second.isNull() ){ + m = NodeManager::currentNM()->mkNode( MULT, it->second, it->first ); + }else{ + m = it->first; + } + }else{ + m = it->second; + } + children.push_back(m); + } + } + veq = children.size()>1 ? NodeManager::currentNM()->mkNode( PLUS, children ) : + (children.size()==1 ? children[0] : NodeManager::currentNM()->mkConst( Rational(0) )); + if( !r.isNegativeOne() ){ + if( r.isOne() ){ + veq = negate(veq); + }else{ + //TODO + return false; + } + } + veq = Rewriter::rewrite( veq ); + veq = NodeManager::currentNM()->mkNode( k, r.sgn()==1 ? v : veq, r.sgn()==1 ? veq : v ); + return true; + } + return false; + }else{ + return false; + } +} + +Node QuantArith::negate( Node t ) { + Node tt = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(-1) ), t ); + tt = Rewriter::rewrite( tt ); + return tt; +} + +Node QuantArith::offset( Node t, int i ) { + Node tt = NodeManager::currentNM()->mkNode( PLUS, NodeManager::currentNM()->mkConst( Rational(i) ), t ); + tt = Rewriter::rewrite( tt ); + return tt; +} + + void QuantRelevance::registerQuantifier( Node f ){ //compute symbols in f std::vector< Node > syms; diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 6a5726cc7..86c7bc3a0 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -28,6 +28,18 @@ namespace CVC4 { namespace theory { +class QuantArith +{ +public: + static bool getMonomial( Node n, std::map< Node, Node >& msum ); + static bool getMonomialSum( Node n, std::map< Node, Node >& msum ); + static bool getMonomialSumLit( Node lit, std::map< Node, Node >& msum ); + static bool isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind k ); + static Node negate( Node t ); + static Node offset( Node t, int i ); +}; + + class QuantRelevance { private: diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 3153a3c64..417b4ae3a 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -254,8 +254,7 @@ void TermDb::computeModelBasisArgAttribute( Node n ){ //determine if it has model basis attribute for( int j=0; j<(int)n.getNumChildren(); j++ ){ if( n[j].getAttribute(ModelBasisAttribute()) ){ - val = 1; - break; + val++; } } ModelBasisArgAttribute mbaa; diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 231d0ee9e..e5154476a 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -83,10 +83,15 @@ public: };/* class TermArgTrie */ +namespace fmcheck { + class FullModelChecker; +} + class TermDb { friend class ::CVC4::theory::QuantifiersEngine; friend class ::CVC4::theory::inst::Trigger; friend class ::CVC4::theory::rrinst::Trigger; + friend class ::CVC4::theory::quantifiers::fmcheck::FullModelChecker; private: /** reference to the quantifiers engine */ QuantifiersEngine* d_quantEngine; diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index cab94fb5c..1f1667522 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -28,8 +28,6 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::inst; -//#define NESTED_PATTERN_SELECTION - /** trigger class constructor */ Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, int matchOption, bool smartTriggers ) : d_quantEngine( qe ), d_f( f ){ @@ -249,11 +247,75 @@ bool Trigger::isUsable( Node n, Node f ){ } } -bool Trigger::isUsableTrigger( Node n, Node f ){ - //return n.getAttribute(InstConstantAttribute())==f && n.getKind()==APPLY_UF; +bool nodeContainsVar( Node n, Node v ){ + if( n==v) { + return true; + }else{ + for( unsigned i=0; i<n.getNumChildren(); i++) { + if( nodeContainsVar(n[i], v) ){ + return true; + } + } + return false; + } +} + +Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) { + if( options::relationalTriggers() ){ + if( n.getKind()==EQUAL || n.getKind()==IFF || n.getKind()==GEQ ){ + Node rtr; + for( unsigned i=0; i<2; i++) { + unsigned j = (i==0) ? 1 : 0; + if( n[j].getKind()==INST_CONSTANT && isUsableTrigger(n[i], f) && !nodeContainsVar( n[i], n[j] ) ) { + rtr = n; + break; + } + } + if( n[0].getType().isInteger() ){ + //try to rearrange? + std::map< Node, Node > m; + if (QuantArith::getMonomialSumLit(n, m) ){ + for( std::map< Node, Node >::iterator it = m.begin(); it!=m.end(); ++it ){ + if( !it->first.isNull() && it->first.getKind()==INST_CONSTANT ){ + Node veq; + if( QuantArith::isolate( it->first, m, veq, n.getKind() ) ){ + int vti = veq[0]==it->first ? 1 : 0; + if( isUsableTrigger(veq[vti], f) && !nodeContainsVar( veq[vti], veq[vti==0 ? 1 : 0]) ){ + rtr = veq; + InstConstantAttribute ica; + rtr.setAttribute(ica,veq[vti].getAttribute(InstConstantAttribute()) ); + } + } + } + } + } + } + if( !rtr.isNull() ){ + Trace("relational-trigger") << "Relational trigger : " << std::endl; + Trace("relational-trigger") << " " << rtr << " (from " << n << ")" << std::endl; + Trace("relational-trigger") << " in quantifier " << f << std::endl; + if( hasPol ){ + Trace("relational-trigger") << " polarity : " << pol << std::endl; + } + Node rtr2 = (hasPol && pol) ? rtr.negate() : rtr; + InstConstantAttribute ica; + rtr2.setAttribute(ica,rtr.getAttribute(InstConstantAttribute()) ); + return rtr2; + } + } + } bool usable = n.getAttribute(InstConstantAttribute())==f && isAtomicTrigger( n ) && isUsable( n, f ); Trace("usable") << n << " usable : " << usable << std::endl; - return usable; + if( usable ){ + return n; + }else{ + return Node::null(); + } +} + +bool Trigger::isUsableTrigger( Node n, Node f ){ + Node nu = getIsUsableTrigger(n,f); + return !nu.isNull(); } bool Trigger::isAtomicTrigger( Node n ){ @@ -274,55 +336,51 @@ bool Trigger::isSimpleTrigger( Node n ){ } -bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt ){ +bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt, bool pol, bool hasPol ){ if( patMap.find( n )==patMap.end() ){ patMap[ n ] = false; + bool newHasPol = (n.getKind()==IFF || n.getKind()==XOR) ? false : hasPol; + bool newPol = n.getKind()==NOT ? !pol : pol; if( tstrt==TS_MIN_TRIGGER ){ if( n.getKind()==FORALL ){ -#ifdef NESTED_PATTERN_SELECTION - //return collectPatTerms2( qe, f, qe->getOrCreateCounterexampleBody( n ), patMap, tstrt ); - return collectPatTerms2( qe, f, qe->getBoundBody( n ), patMap, tstrt ); -#else return false; -#endif }else{ bool retVal = false; for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( collectPatTerms2( qe, f, n[i], patMap, tstrt ) ){ + bool newPol2 = (n.getKind()==IMPLIES && i==0) ? !newPol : newPol; + bool newHasPol2 = (n.getKind()==ITE && i==0) ? false : newHasPol; + if( collectPatTerms2( qe, f, n[i], patMap, tstrt, newPol2, newHasPol2 ) ){ retVal = true; } } if( retVal ){ return true; - }else if( isUsableTrigger( n, f ) ){ - patMap[ n ] = true; - return true; }else{ - return false; + Node nu = getIsUsableTrigger( n, f, pol, hasPol ); + if( !nu.isNull() ){ + patMap[ nu ] = true; + return true; + }else{ + return false; + } } } }else{ bool retVal = false; - if( isUsableTrigger( n, f ) ){ - patMap[ n ] = true; + Node nu = getIsUsableTrigger( n, f, pol, hasPol ); + if( !nu.isNull() ){ + patMap[ nu ] = true; if( tstrt==TS_MAX_TRIGGER ){ return true; }else{ retVal = true; } } - if( n.getKind()==FORALL ){ -#ifdef NESTED_PATTERN_SELECTION - //if( collectPatTerms2( qe, f, qe->getOrCreateCounterexampleBody( n ), patMap, tstrt ) ){ - // retVal = true; - //} - if( collectPatTerms2( qe, f, qe->getBoundBody( n ), patMap, tstrt ) ){ - retVal = true; - } -#endif - }else{ + if( n.getKind()!=FORALL ){ for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( collectPatTerms2( qe, f, n[i], patMap, tstrt ) ){ + bool newPol2 = (n.getKind()==IMPLIES && i==0) ? !newPol : newPol; + bool newHasPol2 = (n.getKind()==ITE && i==0) ? false : newHasPol; + if( collectPatTerms2( qe, f, n[i], patMap, tstrt, newPol2, newHasPol2 ) ){ retVal = true; } } @@ -367,7 +425,7 @@ void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vecto } } } - collectPatTerms2( qe, f, n, patMap, tstrt ); + collectPatTerms2( qe, f, n, patMap, tstrt, true, true ); for( std::map< Node, bool >::iterator it = patMap.begin(); it != patMap.end(); ++it ){ if( it->second ){ patTerms.push_back( it->first ); diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h index ca9124751..28fb2acda 100644 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h @@ -92,8 +92,9 @@ public: private: /** is subterm of trigger usable */ static bool isUsable( Node n, Node f ); + static Node getIsUsableTrigger( Node n, Node f, bool pol = true, bool hasPol = false ); /** collect all APPLY_UF pattern terms for f in n */ - static bool collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt ); + static bool collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt, bool pol, bool hasPol ); public: //different strategies for choosing trigger terms enum { diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 0bb0f1f79..ef8169433 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -27,6 +27,7 @@ #include "theory/quantifiers/trigger.h" #include "theory/rewriterules/efficient_e_matching.h" #include "theory/rewriterules/rr_trigger.h" +#include "theory/quantifiers/bounded_integers.h" using namespace std; using namespace CVC4; @@ -60,8 +61,12 @@ d_lemmas_produced_c(u){ if( options::finiteModelFind() ){ d_model_engine = new quantifiers::ModelEngine( c, this ); d_modules.push_back( d_model_engine ); + + d_bint = new quantifiers::BoundedIntegers( c, this ); + d_modules.push_back( d_bint ); }else{ d_model_engine = NULL; + d_bint = NULL; } //options diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index bfa19bb98..2ff2100b2 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -56,7 +56,7 @@ public: virtual void assertNode( Node n ) = 0; virtual void propagate( Theory::Effort level ){} virtual Node getNextDecisionRequest() { return TNode::null(); } - virtual Node explain(TNode n) = 0; + virtual Node explain(TNode n) { return TNode::null(); } };/* class QuantifiersModule */ namespace quantifiers { @@ -64,6 +64,7 @@ namespace quantifiers { class ModelEngine; class TermDb; class FirstOrderModel; + class BoundedIntegers; }/* CVC4::theory::quantifiers */ namespace inst { @@ -99,6 +100,8 @@ private: std::map< Node, QuantPhaseReq* > d_phase_reqs; /** efficient e-matcher */ EfficientEMatcher* d_eem; + /** bounded integers utility */ + quantifiers::BoundedIntegers * d_bint; private: /** list of all quantifiers seen */ std::vector< Node > d_quants; @@ -155,6 +158,8 @@ public: void getPhaseReqTerms( Node f, std::vector< Node >& nodes ); /** get efficient e-matching utility */ EfficientEMatcher* getEfficientEMatcher() { return d_eem; } + /** get bounded integers utility */ + quantifiers::BoundedIntegers * getBoundedIntegers() { return d_bint; } public: /** initialize */ void finishInit(); diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index f6da32bbf..fe3e39d45 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -14,6 +14,7 @@ #include "theory/rep_set.h" #include "theory/type_enumerator.h" +#include "theory/quantifiers/bounded_integers.h" using namespace std; using namespace CVC4; @@ -99,25 +100,33 @@ RepSetIterator::RepSetIterator( RepSet* rs ) : d_rep_set( rs ){ } -bool RepSetIterator::setQuantifier( Node f ){ +int RepSetIterator::domainSize( int i ) { + if( d_enum_type[i]==ENUM_DOMAIN_ELEMENTS ){ + return d_domain[i].size(); + }else{ + return d_domain[i][0]; + } +} + +bool RepSetIterator::setQuantifier( QuantifiersEngine * qe, Node f ){ Assert( d_types.empty() ); //store indicies for( size_t i=0; i<f[0].getNumChildren(); i++ ){ d_types.push_back( f[0][i].getType() ); } - return initialize(); + return initialize(qe, f); } -bool RepSetIterator::setFunctionDomain( Node op ){ +bool RepSetIterator::setFunctionDomain( QuantifiersEngine * qe, Node op ){ Assert( d_types.empty() ); TypeNode tn = op.getType(); for( size_t i=0; i<tn.getNumChildren()-1; i++ ){ d_types.push_back( tn[i] ); } - return initialize(); + return initialize(qe, Node::null()); } -bool RepSetIterator::initialize(){ +bool RepSetIterator::initialize(QuantifiersEngine * qe, Node f){ for( size_t i=0; i<d_types.size(); i++ ){ d_index.push_back( 0 ); //store default index order @@ -126,13 +135,48 @@ bool RepSetIterator::initialize(){ //store default domain d_domain.push_back( RepDomain() ); TypeNode tn = d_types[i]; + bool isSet = false; if( tn.isSort() ){ if( !d_rep_set->hasType( tn ) ){ Node var = NodeManager::currentNM()->mkSkolem( "repSet_$$", tn, "is a variable created by the RepSetIterator" ); Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn << std::endl; d_rep_set->add( var ); } - }else if( tn.isInteger() || tn.isReal() ){ + }else if( tn.isInteger() ){ + //check if it is bound + if( !f.isNull() && qe && qe->getBoundedIntegers() ){ + Node l = qe->getBoundedIntegers()->getLowerBoundValue( f, f[0][i] ); + Node u = qe->getBoundedIntegers()->getUpperBoundValue( f, f[0][i] ); + if( !l.isNull() && !u.isNull() ){ + Trace("bound-int-reps") << "Can limit bounds of " << f[0][i] << " to " << l << "..." << u << std::endl; + Node range = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MINUS, u, l ) ); + Node ra = Rewriter::rewrite( NodeManager::currentNM()->mkNode( LEQ, range, NodeManager::currentNM()->mkConst( Rational( 9999 ) ) ) ); + if( ra==NodeManager::currentNM()->mkConst(true) ){ + long rr = range.getConst<Rational>().getNumerator().getLong()+1; + if (rr<0) { + Trace("bound-int-reps") << "Empty bound range." << std::endl; + //empty + d_enum_type.push_back( ENUM_DOMAIN_ELEMENTS ); + }else{ + Trace("bound-int-reps") << "Actual bound range is " << rr << std::endl; + d_lower_bounds[i] = l; + d_domain[i].push_back( (int)rr ); + d_enum_type.push_back( ENUM_RANGE ); + } + isSet = true; + }else{ + Trace("fmf-incomplete") << "Incomplete because of integer quantification, bounds are too big." << std::endl; + d_incomplete = true; + } + }else{ + Trace("fmf-incomplete") << "Incomplete because of integer quantification, no bounds found." << std::endl; + d_incomplete = true; + } + }else{ + Trace("fmf-incomplete") << "Incomplete because of integer quantification." << std::endl; + d_incomplete = true; + } + }else if( tn.isReal() ){ Trace("fmf-incomplete") << "Incomplete because of infinite type " << tn << std::endl; d_incomplete = true; //enumerate if the sort is reasonably small, the upper bound of 128 is chosen arbitrarily for now @@ -142,12 +186,15 @@ bool RepSetIterator::initialize(){ Trace("fmf-incomplete") << "Incomplete because of unknown type " << tn << std::endl; d_incomplete = true; } - if( d_rep_set->hasType( tn ) ){ - for( size_t j=0; j<d_rep_set->d_type_reps[tn].size(); j++ ){ - d_domain[i].push_back( j ); + if( !isSet ){ + d_enum_type.push_back( ENUM_DOMAIN_ELEMENTS ); + if( d_rep_set->hasType( tn ) ){ + for( size_t j=0; j<d_rep_set->d_type_reps[tn].size(); j++ ){ + d_domain[i].push_back( j ); + } + }else{ + return false; } - }else{ - return false; } } return true; @@ -161,7 +208,7 @@ void RepSetIterator::setIndexOrder( std::vector< int >& indexOrder ){ d_var_order[d_index_order[i]] = i; } } - +/* void RepSetIterator::setDomain( std::vector< RepDomain >& domain ){ d_domain.clear(); d_domain.insert( d_domain.begin(), domain.begin(), domain.end() ); @@ -172,14 +219,14 @@ void RepSetIterator::setDomain( std::vector< RepDomain >& domain ){ } } } - +*/ void RepSetIterator::increment2( int counter ){ Assert( !isFinished() ); #ifdef DISABLE_EVAL_SKIP_MULTIPLE counter = (int)d_index.size()-1; #endif //increment d_index - while( counter>=0 && d_index[counter]==(int)(d_domain[counter].size()-1) ){ + while( counter>=0 && d_index[counter]==(int)(domainSize(counter)-1) ){ counter--; } if( counter==-1 ){ @@ -203,10 +250,17 @@ bool RepSetIterator::isFinished(){ } Node RepSetIterator::getTerm( int i ){ - TypeNode tn = d_types[d_index_order[i]]; - Assert( d_rep_set->d_type_reps.find( tn )!=d_rep_set->d_type_reps.end() ); int index = d_index_order[i]; - return d_rep_set->d_type_reps[tn][d_domain[index][d_index[index]]]; + if( d_enum_type[index]==ENUM_DOMAIN_ELEMENTS ){ + TypeNode tn = d_types[index]; + Assert( d_rep_set->d_type_reps.find( tn )!=d_rep_set->d_type_reps.end() ); + return d_rep_set->d_type_reps[tn][d_domain[index][d_index[index]]]; + }else{ + Node t = NodeManager::currentNM()->mkNode(PLUS, d_lower_bounds[index], + NodeManager::currentNM()->mkConst( Rational(d_index[index]) ) ); + t = Rewriter::rewrite( t ); + return t; + } } void RepSetIterator::debugPrint( const char* c ){ diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h index 24fa7473e..b92d9d2c6 100644 --- a/src/theory/rep_set.h +++ b/src/theory/rep_set.h @@ -23,6 +23,8 @@ namespace CVC4 { namespace theory { +class QuantifiersEngine; + /** this class stores a representative set */ class RepSet { public: @@ -53,15 +55,26 @@ typedef std::vector< int > RepDomain; /** this class iterates over a RepSet */ class RepSetIterator { private: + enum { + ENUM_DOMAIN_ELEMENTS, + ENUM_RANGE, + }; + //initialize function - bool initialize(); + bool initialize(QuantifiersEngine * qe, Node f); + //enumeration type? + std::vector< int > d_enum_type; + //for enum ranges + std::map< int, Node > d_lower_bounds; + //domain size + int domainSize( int i ); public: RepSetIterator( RepSet* rs ); ~RepSetIterator(){} //set that this iterator will be iterating over instantiations for a quantifier - bool setQuantifier( Node f ); + bool setQuantifier( QuantifiersEngine * qe, Node f ); //set that this iterator will be iterating over the domain of a function - bool setFunctionDomain( Node op ); + bool setFunctionDomain( QuantifiersEngine * qe, Node op ); public: //pointer to model RepSet* d_rep_set; @@ -90,7 +103,7 @@ public: /** set index order */ void setIndexOrder( std::vector< int >& indexOrder ); /** set domain */ - void setDomain( std::vector< RepDomain >& domain ); + //void setDomain( std::vector< RepDomain >& domain ); /** increment the iterator at index=counter */ void increment2( int counter ); /** increment the iterator */ diff --git a/src/theory/uf/options b/src/theory/uf/options index 33d1255ef..bea11621a 100644 --- a/src/theory/uf/options +++ b/src/theory/uf/options @@ -30,5 +30,7 @@ option ufssSimpleCliques --uf-ss-simple-cliques bool :default true always use simple clique lemmas for uf strong solver option ufssDiseqPropagation --uf-ss-deq-prop bool :default false eagerly propagate disequalities for uf strong solver +option ufssMinimalModel /--disable-uf-ss-min-model bool :default true + disable finding a minimal model in uf strong solver endmodule diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp index 228cfd2c4..2c853a4fa 100644 --- a/src/theory/uf/theory_uf_model.cpp +++ b/src/theory/uf/theory_uf_model.cpp @@ -17,6 +17,7 @@ #include "theory/uf/equality_engine.h" #include "theory/uf/theory_uf.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/options.h" #define RECONSIDER_FUNC_DEFAULT_VALUE #define USE_PARTIAL_DEFAULT_VALUES @@ -309,19 +310,21 @@ void UfModelTreeGenerator::setValue( TheoryModel* m, Node n, Node v, bool ground if( !ground ){ int defSize = (int)d_defaults.size(); for( int i=0; i<defSize; i++ ){ - bool isGround; //for soundness, to allow variable order-independent function interpretations, // we must ensure that the intersection of all default terms // is also defined. //for example, if we have that f( e, a ) = ..., and f( b, e ) = ..., // then we must define f( b, a ). - Node ni = getIntersection( m, n, d_defaults[i], isGround ); - if( !ni.isNull() ){ - //if the intersection exists, and is not already defined - if( d_set_values[0][ isGround ? 1 : 0 ].find( ni )==d_set_values[0][ isGround ? 1 : 0 ].end() && - d_set_values[1][ isGround ? 1 : 0 ].find( ni )==d_set_values[1][ isGround ? 1 : 0 ].end() ){ - //use the current value - setValue( m, ni, v, isGround, false ); + if (!options::fmfFullModelCheck()) { + bool isGround; + Node ni = getIntersection( m, n, d_defaults[i], isGround ); + if( !ni.isNull() ){ + //if the intersection exists, and is not already defined + if( d_set_values[0][ isGround ? 1 : 0 ].find( ni )==d_set_values[0][ isGround ? 1 : 0 ].end() && + d_set_values[1][ isGround ? 1 : 0 ].find( ni )==d_set_values[1][ isGround ? 1 : 0 ].end() ){ + //use the current value + setValue( m, ni, v, isGround, false ); + } } } } diff --git a/src/theory/uf/theory_uf_model.h b/src/theory/uf/theory_uf_model.h index 12c1cf244..2149a6583 100644 --- a/src/theory/uf/theory_uf_model.h +++ b/src/theory/uf/theory_uf_model.h @@ -144,18 +144,12 @@ public: void debugPrint( std::ostream& out, TheoryModel* m, int ind = 0 ){ d_tree.debugPrint( out, m, d_index_order, ind ); } -private: - //helper for to ITE function. - static Node toIte2( Node fm_node, std::vector< Node >& args, int index, Node defaultNode ); -public: - /** to ITE function for function model nodes */ - static Node toIte( Node fm_node, std::vector< Node >& args ) { return toIte2( fm_node, args, 0, Node::null() ); } - static Node toIte( TypeNode type, Node fm_node, const char* argPrefix ); }; + class UfModelTreeGenerator { -private: +public: //store for set values Node d_default_value; std::map< Node, Node > d_set_values[2][2]; diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index d64f7df60..e868460f8 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -595,9 +595,11 @@ void StrongSolverTheoryUF::SortModel::check( Theory::Effort level, OutputChannel if( d_regions[i]->d_valid ){ std::vector< Node > clique; if( d_regions[i]->check( level, d_cardinality, clique ) ){ - //add clique lemma - addCliqueLemma( clique, out ); - return; + if( options::ufssMinimalModel() ){ + //add clique lemma + addCliqueLemma( clique, out ); + return; + } }else{ Trace("uf-ss-debug") << "No clique in Region #" << i << std::endl; } @@ -659,13 +661,17 @@ void StrongSolverTheoryUF::SortModel::check( Theory::Effort level, OutputChannel //naive strategy, force region combination involving the first valid region for( int i=0; i<(int)d_regions_index; i++ ){ if( d_regions[i]->d_valid ){ - forceCombineRegion( i, false ); - recheck = true; - break; + int fcr = forceCombineRegion( i, false ); + Trace("uf-ss-debug") << "Combined regions " << i << " " << fcr << std::endl; + if( options::ufssMinimalModel() || fcr!=-1 ){ + recheck = true; + break; + } } } } if( recheck ){ + Trace("uf-ss-debug") << "Must recheck." << std::endl; check( level, out ); } } @@ -869,8 +875,10 @@ void StrongSolverTheoryUF::SortModel::checkRegion( int ri, bool checkCombine ){ //now check if region is in conflict std::vector< Node > clique; if( d_regions[ri]->check( Theory::EFFORT_STANDARD, d_cardinality, clique ) ){ - //explain clique - addCliqueLemma( clique, &d_thss->getOutputChannel() ); + if( options::ufssMinimalModel() ){ + //explain clique + addCliqueLemma( clique, &d_thss->getOutputChannel() ); + } } } } @@ -1013,8 +1021,8 @@ void StrongSolverTheoryUF::SortModel::allocateCardinality( OutputChannel* out ){ } bool StrongSolverTheoryUF::SortModel::addSplit( Region* r, OutputChannel* out ){ + Node s; if( r->hasSplits() ){ - Node s; if( !options::ufssSmartSplits() ){ //take the first split you find for( NodeBoolMap::iterator it = r->d_splits.begin(); it != r->d_splits.end(); ++it ){ @@ -1038,8 +1046,26 @@ bool StrongSolverTheoryUF::SortModel::addSplit( Region* r, OutputChannel* out ){ } } } + Assert( s!=Node::null() ); + }else{ + if( !options::ufssMinimalModel() ){ + //since candidate clique is not reported, we may need to find splits manually + for ( std::map< Node, Region::RegionNodeInfo* >::iterator it = r->d_nodes.begin(); it != r->d_nodes.end(); ++it ){ + if ( it->second->d_valid ){ + for ( std::map< Node, Region::RegionNodeInfo* >::iterator it2 = r->d_nodes.begin(); it2 != r->d_nodes.end(); ++it2 ){ + if ( it->second!=it2->second && it2->second->d_valid ){ + if( !r->isDisequal( it->first, it2->first, 1 ) ){ + s = NodeManager::currentNM()->mkNode( EQUAL, it->first, it2->first ); + } + } + } + } + } + } + } + if (!s.isNull() ){ //add lemma to output channel - Assert( s!=Node::null() && s.getKind()==EQUAL ); + Assert( s.getKind()==EQUAL ); s = Rewriter::rewrite( s ); Trace("uf-ss-lemma") << "*** Split on " << s << std::endl; if( options::sortInference()) { diff --git a/test/regress/regress0/arith/integers/Makefile.am b/test/regress/regress0/arith/integers/Makefile.am index efd5aa909..c555ba413 100644 --- a/test/regress/regress0/arith/integers/Makefile.am +++ b/test/regress/regress0/arith/integers/Makefile.am @@ -20,9 +20,9 @@ MAKEFLAGS = -k TESTS = \ arith-int-004.cvc \ - arith-int-007.cvc \ arith-int-011.cvc \ arith-int-012.cvc \ + arith-int-013.cvc \ arith-int-022.cvc \ arith-int-024.cvc \ arith-int-042.cvc \ @@ -34,7 +34,7 @@ TESTS = \ arith-int-097.cvc \ arith-int-085.cvc -EXTRA_DIST = $(TESTS) +EXTRA_DIST = $(TESTS) \ arith-int-001.cvc \ arith-int-002.cvc \ arith-int-003.cvc \ @@ -105,7 +105,6 @@ EXTRA_DIST = $(TESTS) arith-int-079.cvc \ arith-int-080.cvc \ arith-int-081.cvc \ - arith-int-082.cvc \ arith-int-083.cvc \ arith-int-086.cvc \ arith-int-087.cvc \ @@ -122,9 +121,11 @@ EXTRA_DIST = $(TESTS) arith-int-099.cvc \ arith-int-100.cvc + FAILING_TESTS = \ - arith-int-024.cvc \ - arith-int-013.cvc + arith-int-007.cvc \ + arith-int-082.cvc \ + arith-int-098.cvc #if CVC4_BUILD_PROFILE_COMPETITION #else diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h index 844fb57d1..3247b8c73 100644 --- a/test/unit/theory/theory_arith_white.h +++ b/test/unit/theory/theory_arith_white.h @@ -60,6 +60,7 @@ class TheoryArithWhite : public CxxTest::TestSuite { TypeNode* d_booleanType; TypeNode* d_realType; + TypeNode* d_intType; const Rational d_zero; const Rational d_one; @@ -120,10 +121,12 @@ public: d_booleanType = new TypeNode(d_nm->booleanType()); d_realType = new TypeNode(d_nm->realType()); + d_intType = new TypeNode(d_nm->integerType()); } void tearDown() { + delete d_intType; delete d_realType; delete d_booleanType; @@ -281,4 +284,37 @@ public: TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), LEMMA); TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), geq0OrLeq1); } + + void testIntNormalForm() { + Node x = d_nm->mkVar(*d_intType); + Node c0 = d_nm->mkConst<Rational>(d_zero); + Node c1 = d_nm->mkConst<Rational>(d_one); + Node c2 = d_nm->mkConst<Rational>(Rational(2)); + + + Node geq0 = d_nm->mkNode(GEQ, x, c0); + Node geq1 = d_nm->mkNode(GEQ, x, c1); + Node geq2 = d_nm->mkNode(GEQ, x, c2); + + TS_ASSERT_EQUALS(Rewriter::rewrite(geq0), geq0); + TS_ASSERT_EQUALS(Rewriter::rewrite(geq1), geq1); + + Node gt0 = d_nm->mkNode(GT, x, c0); + Node gt1 = d_nm->mkNode(GT, x, c1); + + TS_ASSERT_EQUALS(Rewriter::rewrite(gt0), Rewriter::rewrite(geq1)); + TS_ASSERT_EQUALS(Rewriter::rewrite(gt1), Rewriter::rewrite(geq2)); + + Node lt0 = d_nm->mkNode(LT, x, c0); + Node lt1 = d_nm->mkNode(LT, x, c1); + + TS_ASSERT_EQUALS(Rewriter::rewrite(lt0), Rewriter::rewrite(geq0.notNode())); + TS_ASSERT_EQUALS(Rewriter::rewrite(lt1), Rewriter::rewrite(geq1.notNode())); + + Node leq0 = d_nm->mkNode(LEQ, x, c0); + Node leq1 = d_nm->mkNode(LEQ, x, c1); + + TS_ASSERT_EQUALS(Rewriter::rewrite(leq0), Rewriter::rewrite(geq1.notNode())); + TS_ASSERT_EQUALS(Rewriter::rewrite(leq1), Rewriter::rewrite(geq2.notNode())); + } }; |