diff options
-rw-r--r-- | src/theory/quantifiers/cegqi/ceg_instantiator.cpp | 17 | ||||
-rw-r--r-- | src/theory/quantifiers/cegqi/ceg_instantiator.h | 8 | ||||
-rw-r--r-- | src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp | 11 | ||||
-rw-r--r-- | src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp | 11 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/trigger.cpp | 10 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/trigger.h | 7 | ||||
-rw-r--r-- | test/regress/regress0/quantifiers/Makefile.am | 4 | ||||
-rw-r--r-- | test/regress/regress0/quantifiers/cegqi-nl-simp.cvc | 2 | ||||
-rw-r--r-- | test/regress/regress0/quantifiers/cegqi-nl-sq.smt2 | 5 |
9 files changed, 45 insertions, 30 deletions
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index d7d46bb4b..358efede7 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -127,6 +127,23 @@ bool CegInstantiator::isEligible( Node n ) { return d_inelig.find( n )==d_inelig.end(); } +bool CegInstantiator::isCbqiKind(Kind k) +{ + if (quantifiers::TermUtil::isBoolConnective(k) || k == PLUS || k == GEQ + || k == EQUAL + || k == MULT + || k == NONLINEAR_MULT) + { + return true; + } + else + { + // CBQI typically works for satisfaction-complete theories + TheoryId t = kindToTheoryId(k); + return t == THEORY_BV || t == THEORY_DATATYPES || t == THEORY_BOOL; + } +} + bool CegInstantiator::hasVariable( Node n, Node pv ) { computeProgVars( n ); return d_prog_var[n].find( pv )!=d_prog_var[n].end(); diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.h b/src/theory/quantifiers/cegqi/ceg_instantiator.h index c12890b83..6cbc7418c 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.h @@ -297,6 +297,14 @@ class CegInstantiator { bool useVtsInfinity() { return d_use_vts_inf; } /** are we processing a nested quantified formula? */ bool hasNestedQuantification() { return d_is_nested_quant; } + /** Is k a kind for which counterexample-guided instantiation is possible? + * + * This typically corresponds to kinds that correspond to operators that + * have total interpretations and are a part of the signature of + * satisfaction complete theories (see Reynolds et al., CAV 2015). + */ + static bool isCbqiKind(Kind k); + private: /** quantified formula associated with this instantiator */ QuantifiersEngine* d_qe; diff --git a/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp index bb210edcc..b526fb1ee 100644 --- a/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp @@ -155,12 +155,11 @@ int ArithInstantiator::solve_arith( CegInstantiator * ci, Node pv, Node atom, No } Trace("cegqi-arith-debug") << pv << " " << atom.getKind() << " " << val << std::endl; } - if( options::cbqiAll() ){ - // when not pure LIA/LRA, we must check whether the lhs contains pv - if( TermUtil::containsTerm( val, pv ) ){ - Trace("cegqi-arith-debug") << "fail : contains bad term" << std::endl; - return 0; - } + // when not pure LIA/LRA, we must check whether the lhs contains pv + if (TermUtil::containsTerm(val, pv)) + { + Trace("cegqi-arith-debug") << "fail : contains bad term" << std::endl; + return 0; } if( pvtn.isInteger() && ( ( !veq_c.isNull() && !veq_c.getType().isInteger() ) || !val.getType().isInteger() ) ){ //redo, split integer/non-integer parts diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp index 8de3dbfcb..c07ddcd8f 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp @@ -25,7 +25,6 @@ #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers/ematching/trigger.h" #include "theory/theory_engine.h" using namespace std; @@ -484,13 +483,13 @@ bool InstStrategyCbqi::hasNonCbqiOperator( Node n, std::map< Node, bool >& visit if( visited.find( n )==visited.end() ){ visited[n] = true; if( n.getKind()!=BOUND_VARIABLE && TermUtil::hasBoundVarAttr( n ) ){ - if( !inst::Trigger::isCbqiKind( n.getKind() ) ){ + if (!CegInstantiator::isCbqiKind(n.getKind())) + { Trace("cbqi-debug2") << "Non-cbqi kind : " << n.getKind() << " in " << n << std::endl; return true; - }else if( n.getKind()==MULT && ( n.getNumChildren()!=2 || !n[0].isConst() ) ){ - Trace("cbqi-debug2") << "Non-linear arithmetic : " << n << std::endl; - return true; - }else if( n.getKind()==FORALL ){ + } + else if (n.getKind() == FORALL || n.getKind() == CHOICE) + { return hasNonCbqiOperator( n[1], visited ); }else{ for( unsigned i=0; i<n.getNumChildren(); i++ ){ diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index b73c3368d..430d261a1 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -393,16 +393,6 @@ bool Trigger::isRelationalTrigger( Node n ) { bool Trigger::isRelationalTriggerKind( Kind k ) { return k==EQUAL || k==GEQ; } - -bool Trigger::isCbqiKind( Kind k ) { - if( quantifiers::TermUtil::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 || t == THEORY_BOOL; - } -} bool Trigger::isSimpleTrigger( Node n ){ Node t = n.getKind()==NOT ? n[0] : n; diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h index e91a87e58..cd10e4f8a 100644 --- a/src/theory/quantifiers/ematching/trigger.h +++ b/src/theory/quantifiers/ematching/trigger.h @@ -313,13 +313,6 @@ class Trigger { static bool isRelationalTrigger( Node n ); /** Is k a relational trigger kind? */ static bool isRelationalTriggerKind( Kind k ); - /** Is k a kind for which counterexample-guided instantiation is possible? - * - * This typically corresponds to kinds that correspond to operators that - * have total interpretations and are a part of the signature of - * satisfaction complete theories (see Reynolds et al., CAV 2015). - */ - static bool isCbqiKind( Kind k ); /** is n a simple trigger (see inst_match_generator.h)? */ static bool isSimpleTrigger( Node n ); /** is n a Boolean term trigger, e.g. ite( x, BV1, BV0 )? */ diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index 1711c301e..809297863 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -71,7 +71,9 @@ TESTS = \ qbv-test-invert-concat-1.smt2 \ qbv-test-invert-sign-extend.smt2 \ clock-10.smt2 \ - lra-triv-gn.smt2 + lra-triv-gn.smt2 \ + cegqi-nl-simp.cvc \ + cegqi-nl-sq.smt2 EXTRA_DIST = $(TESTS) \ bug291.smt2.expect diff --git a/test/regress/regress0/quantifiers/cegqi-nl-simp.cvc b/test/regress/regress0/quantifiers/cegqi-nl-simp.cvc new file mode 100644 index 000000000..63cf52fd6 --- /dev/null +++ b/test/regress/regress0/quantifiers/cegqi-nl-simp.cvc @@ -0,0 +1,2 @@ +% EXPECT: valid +QUERY FORALL (x:INT) : EXISTS (y:INT) : (x*y=x) ; diff --git a/test/regress/regress0/quantifiers/cegqi-nl-sq.smt2 b/test/regress/regress0/quantifiers/cegqi-nl-sq.smt2 new file mode 100644 index 000000000..703f816d5 --- /dev/null +++ b/test/regress/regress0/quantifiers/cegqi-nl-sq.smt2 @@ -0,0 +1,5 @@ +(set-logic NIA) +(set-info :status unsat) +(assert (not (exists ((?X Int)) (= (* ?X ?X) ?X)))) +(check-sat) +(exit) |