diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-06-17 15:55:56 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-06-17 15:57:28 -0500 |
commit | 1a2547995acc5a98c8969e628ac5e1c45b0efe94 (patch) | |
tree | 0d9abd19ba7b3b742da3e745da00c0457237f84b /src/theory/quantifiers | |
parent | 0348b525a951a8709f9dc4b5757ce0bcb48a9472 (diff) |
Support for separation logic. Enable cbqi by default for pure BV.
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/model_engine.cpp | 36 | ||||
-rw-r--r-- | src/theory/quantifiers/quant_util.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/trigger.cpp | 9 |
5 files changed, 27 insertions, 26 deletions
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index d2637a555..523d868b5 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -190,7 +190,7 @@ bool InstStrategyCbqi::hasNonCbqiOperator( Node n, std::map< Node, bool >& visit bool InstStrategyCbqi::hasNonCbqiVariable( Node q ){ for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ TypeNode tn = q[0][i].getType(); - if( !tn.isInteger() && !tn.isReal() && !tn.isBoolean() ){ + if( !tn.isInteger() && !tn.isReal() && !tn.isBoolean() && !tn.isBitVector() ){ if( options::cbqiSplx() ){ return true; }else{ @@ -242,7 +242,7 @@ Node InstStrategyCbqi::getNextDecisionRequest(){ Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q ); bool value; if( !d_quantEngine->getValuation().hasSatValue( cel, value ) ){ - Trace("cbqi-debug2") << "CBQI: get next decision " << cel << std::endl; + Trace("cbqi-dec") << "CBQI: get next decision " << cel << std::endl; return cel; } } diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index f855154af..5d575969f 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -153,27 +153,23 @@ int ModelEngine::checkModel(){ //d_quantEngine->getEqualityQuery()->flattenRepresentatives( fm->d_rep_set.d_type_reps ); //for debugging - if( Trace.isOn("model-engine") || Trace.isOn("model-engine-debug") ){ - 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("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl; - if( Trace.isOn("model-engine-debug") ){ - Trace("model-engine-debug") << " Reps : "; - for( size_t i=0; i<it->second.size(); i++ ){ - Trace("model-engine-debug") << it->second[i] << " "; - } - Trace("model-engine-debug") << std::endl; - Trace("model-engine-debug") << " Term reps : "; - for( size_t i=0; i<it->second.size(); i++ ){ - Node r = d_quantEngine->getEqualityQuery()->getInternalRepresentative( it->second[i], Node::null(), 0 ); - Trace("model-engine-debug") << r << " "; - } - Trace("model-engine-debug") << std::endl; - Node mbt = d_quantEngine->getTermDatabase()->getModelBasisTerm(it->first); - Trace("model-engine-debug") << " Basis term : " << mbt << std::endl; - } + 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("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl; + Trace("model-engine-debug") << " Reps : "; + for( size_t i=0; i<it->second.size(); i++ ){ + Trace("model-engine-debug") << it->second[i] << " "; + } + Trace("model-engine-debug") << std::endl; + Trace("model-engine-debug") << " Term reps : "; + for( size_t i=0; i<it->second.size(); i++ ){ + Node r = d_quantEngine->getEqualityQuery()->getInternalRepresentative( it->second[i], Node::null(), 0 ); + Trace("model-engine-debug") << r << " "; } + Trace("model-engine-debug") << std::endl; + Node mbt = d_quantEngine->getTermDatabase()->getModelBasisTerm(it->first); + Trace("model-engine-debug") << " Basis term : " << mbt << std::endl; } } diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index 437f1bddf..b9aab0236 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -382,7 +382,7 @@ void QuantPhaseReq::computePhaseReqs( Node n, bool polarity, std::map< Node, int } void QuantPhaseReq::getPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol ) { - if( n.getKind()==AND || n.getKind()==OR ){ + if( n.getKind()==AND || n.getKind()==OR || n.getKind()==SEP_STAR ){ newHasPol = hasPol; newPol = pol; }else if( n.getKind()==IMPLIES ){ diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index c34d86497..9f222431e 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1925,7 +1925,7 @@ bool TermDb::containsUninterpretedConstant( Node n ) { bool ret = false; if( n.getKind()==UNINTERPRETED_CONSTANT ){ ret = true; - }else{ + }else if( n.getKind()!=SEP_NIL ){ //sep.nil has dummy argument FIXME for( unsigned i=0; i<n.getNumChildren(); i++ ){ if( containsUninterpretedConstant( n[i] ) ){ ret = true; diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 802acc089..ee091919d 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -375,8 +375,13 @@ bool Trigger::isRelationalTriggerKind( Kind k ) { } bool Trigger::isCbqiKind( Kind k ) { - return quantifiers::TermDb::isBoolConnective( k ) || k==PLUS || k==GEQ || k==EQUAL || k==MULT || - k==APPLY_CONSTRUCTOR || k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER; + if( quantifiers::TermDb::isBoolConnective( k ) || k==PLUS || k==GEQ || k==EQUAL || k==MULT ){ + return true; + }else{ + //CBQI typically works for satisfaction-complete theories + TheoryId t = kindToTheoryId( k ); + return t==THEORY_BV || t==THEORY_DATATYPES; + } } bool Trigger::isSimpleTrigger( Node n ){ |