diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-05-15 09:09:51 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-05-15 09:09:51 +0200 |
commit | 3ce21ef9a8b6daa1eef1dbe9af10a84e8c87e413 (patch) | |
tree | 2686fa03573e19593e3395d4097ce1e7943ba04a /src | |
parent | e7439fc0daf1049f59540b9aeb890a52d86a77bd (diff) |
Avoid ensureLiteral on unpreprocessed formulas in cbqi.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/quantifiers/instantiation_engine.cpp | 15 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 9 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.h | 2 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 3 |
5 files changed, 16 insertions, 15 deletions
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 12d6bed8d..f530f7b9d 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -95,21 +95,20 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ Node f = d_quantEngine->getModel()->getAssertedQuantifier( i ); if( doCbqi( f ) && !hasAddedCbqiLemma( f ) ){ d_added_cbqi_lemma[f] = true; - Debug("cbqi") << "Do cbqi for " << f << std::endl; + Trace("cbqi") << "Do cbqi for " << f << std::endl; //add cbqi lemma //get the counterexample literal Node ceLit = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( f ); - if( !ceLit.isNull() ){ + Node ceBody = d_quantEngine->getTermDatabase()->getInstConstantBody( f ); + if( !ceBody.isNull() ){ + //add counterexample lemma + Node lem = NodeManager::currentNM()->mkNode( OR, ceLit.negate(), ceBody.negate() ); //require any decision on cel to be phase=true - //d_quantEngine->getOutputChannel().requirePhase( ceLit, true ); d_quantEngine->addRequirePhase( ceLit, true ); Debug("cbqi-debug") << "Require phase " << ceLit << " = true." << std::endl; //add counterexample lemma - NodeBuilder<> nb(kind::OR); - nb << f << ceLit; - Node lem = nb; + lem = Rewriter::rewrite( lem ); Trace("cbqi") << "Counterexample lemma : " << lem << std::endl; - //d_quantEngine->getOutputChannel().lemma( lem, false, true ); d_quantEngine->addLemma( lem, false ); addedLemma = true; } @@ -125,7 +124,7 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ InstStrategy* is = d_instStrategies[i]; is->processResetInstantiationRound( effort ); } - + //iterate over an internal effort level e int e = 0; int eLimit = effort==Theory::EFFORT_LAST_CALL ? 10 : 2; diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 62eb78679..1082bed23 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -741,6 +741,7 @@ Node TermDb::getInstConstantBody( Node f ){ Node TermDb::getCounterexampleLiteral( Node f ){ if( d_ce_lit.find( f )==d_ce_lit.end() ){ + /* Node ceBody = getInstConstantBody( f ); //check if any variable are of bad types, and fail if so for( size_t i=0; i<d_inst_constants[f].size(); i++ ){ @@ -749,8 +750,10 @@ Node TermDb::getCounterexampleLiteral( Node f ){ return Node::null(); } } + */ + Node g = NodeManager::currentNM()->mkSkolem( "g", NodeManager::currentNM()->booleanType() ); //otherwise, ensure literal - Node ceLit = d_quantEngine->getValuation().ensureLiteral( ceBody.notNode() ); + Node ceLit = d_quantEngine->getValuation().ensureLiteral( g ); d_ce_lit[ f ] = ceLit; } return d_ce_lit[ f ]; @@ -1191,7 +1194,7 @@ bool TermDb::isFunDef( Node q ) { } Node TermDb::getFunDefHead( Node q ) { - //&& ( q[1].getKind()==EQUAL || q[1].getKind()==IFF ) && q[1][0].getKind()==APPLY_UF && + //&& ( q[1].getKind()==EQUAL || q[1].getKind()==IFF ) && q[1][0].getKind()==APPLY_UF && if( q.getKind()==FORALL && q.getNumChildren()==3 ){ for( unsigned i=0; i<q[2].getNumChildren(); i++ ){ if( q[2][i].getKind()==INST_ATTRIBUTE ){ @@ -1972,7 +1975,7 @@ TypeNode TermDbSygus::getArgType( const DatatypeConstructor& c, int i ) { } Node TermDbSygus::minimizeBuiltinTerm( Node n ) { - if( ( n.getKind()==EQUAL || n.getKind()==LEQ || n.getKind()==LT || n.getKind()==GEQ || n.getKind()==GT ) && + if( ( n.getKind()==EQUAL || n.getKind()==LEQ || n.getKind()==LT || n.getKind()==GEQ || n.getKind()==GT ) && ( n[0].getType().isInteger() || n[0].getType().isReal() ) ){ bool changed = false; std::vector< Node > mon[2]; diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index c940b3218..afc607470 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -45,7 +45,7 @@ using namespace CVC4::theory; using namespace CVC4::theory::inst; unsigned QuantifiersModule::needsModel( Theory::Effort e ) { - return QuantifiersEngine::QEFFORT_NONE; + return QuantifiersEngine::QEFFORT_NONE; } eq::EqualityEngine * QuantifiersModule::getEqualityEngine() { diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 6468d4650..e613ef284 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -266,8 +266,6 @@ public: Node getInstantiation( Node f, std::vector< Node >& terms ); /** do substitution */ Node getSubstitute( Node n, std::vector< Node >& terms ); - /** exist instantiation ? */ - //bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false ); /** add lemma lem */ bool addLemma( Node lem, bool doCache = true ); /** add require phase */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index d0a1eb696..bbeec5125 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -428,7 +428,8 @@ void TheoryEngine::check(Theory::Effort effort) { } } - Debug("theory") << "TheoryEngine::check(" << effort << "): done, we are " << (d_inConflict ? "unsat" : "sat") << (d_lemmasAdded ? " with new lemmas" : " with no new lemmas") << endl; + Debug("theory") << "TheoryEngine::check(" << effort << "): done, we are " << (d_inConflict ? "unsat" : "sat") << (d_lemmasAdded ? " with new lemmas" : " with no new lemmas"); + Debug("theory") << ", need check = " << needCheck() << endl; if(!d_inConflict && Theory::fullEffort(effort) && d_masterEqualityEngine != NULL && !d_lemmasAdded) { AlwaysAssert(d_masterEqualityEngine->consistent()); |