diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-25 16:15:10 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-25 16:15:10 +0100 |
commit | 29bdfca306a7cd35801c7d9cb3023d78a8b82a1f (patch) | |
tree | 1c50ca8eb48010b3f327d3d9ada06161e27d9834 /src/theory/quantifiers/theory_quantifiers.cpp | |
parent | 38e077ab219082ee044c2e17ed809e3519c80842 (diff) |
Fix bug in --term-db-mode=relevant with variable triggers. Support inst-closure predicate and mode --term-db-inst-closure. Minor changes to theory_quantifiers.
Diffstat (limited to 'src/theory/quantifiers/theory_quantifiers.cpp')
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers.cpp | 33 |
1 files changed, 15 insertions, 18 deletions
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 5c68e52a7..de0f98af6 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -35,7 +35,6 @@ using namespace CVC4::theory::quantifiers; TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo), - d_numRestarts(0), d_masterEqualityEngine(0) { d_numInstantiations = 0; @@ -97,6 +96,10 @@ Node TheoryQuantifiers::getValue(TNode n) { } } +void TheoryQuantifiers::computeCareGraph() { + //do nothing +} + void TheoryQuantifiers::collectModelInfo(TheoryModel* m, bool fullModel) { if(fullModel) { for(assertions_iterator i = facts_begin(); i != facts_end(); ++i) { @@ -126,12 +129,22 @@ void TheoryQuantifiers::check(Effort e) { case kind::FORALL: assertUniversal( assertion ); break; + case kind::INST_CLOSURE: + getQuantifiersEngine()->addTermToDatabase( assertion[0], false, true ); + break; + case kind::EQUAL: + //do nothing + break; case kind::NOT: { switch( assertion[0].getKind()) { case kind::FORALL: assertExistential( assertion ); break; + case kind::EQUAL: + //do nothing + break; + case kind::INST_CLOSURE: //cannot negate inst closure default: Unhandled(assertion[0].getKind()); break; @@ -182,23 +195,7 @@ bool TheoryQuantifiers::flipDecision(){ //}else{ // return false; //} - - if( !d_out->flipDecision() ){ - return restart(); - } - return true; -} - -bool TheoryQuantifiers::restart(){ - static const int restartLimit = 0; - if( d_numRestarts==restartLimit ){ - Debug("quantifiers-flip") << "No more restarts." << std::endl; - return false; - }else{ - d_numRestarts++; - Debug("quantifiers-flip") << "Do restart." << std::endl; - return true; - } + return false; } void TheoryQuantifiers::setUserAttribute(const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value){ |