summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/smt/smt_engine.cpp3
-rw-r--r--src/theory/quantifiers/candidate_generator.cpp32
-rw-r--r--src/theory/quantifiers/candidate_generator.h2
-rw-r--r--src/theory/quantifiers/inst_strategy_e_matching.cpp22
-rw-r--r--src/theory/quantifiers/trigger.cpp24
-rw-r--r--src/theory/quantifiers/trigger.h1
-rw-r--r--src/theory/quantifiers_engine.cpp4
-rw-r--r--src/theory/quantifiers_engine.h1
-rw-r--r--test/regress/regress0/push-pop/Makefile.am3
-rw-r--r--test/regress/regress0/push-pop/inc-define.smt29
10 files changed, 80 insertions, 21 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 5e97158ca..bbaa07af5 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2123,6 +2123,8 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const
void SmtEngine::defineFunction(Expr func,
const std::vector<Expr>& formals,
Expr formula) {
+ SmtScope smts(this);
+ doPendingPops();
Trace("smt") << "SMT defineFunction(" << func << ")" << endl;
for(std::vector<Expr>::const_iterator i = formals.begin(); i != formals.end(); ++i) {
if((*i).getKind() != kind::BOUND_VARIABLE) {
@@ -2141,7 +2143,6 @@ void SmtEngine::defineFunction(Expr func,
DefineFunctionCommand c(ss.str(), func, formals, formula);
addToModelCommandAndDump(c, ExprManager::VAR_FLAG_DEFINED, true, "declarations");
- SmtScope smts(this);
PROOF( if (options::checkUnsatCores()) {
d_defineCommands.push_back(c.clone());
diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp
index 680be77da..1f68884b6 100644
--- a/src/theory/quantifiers/candidate_generator.cpp
+++ b/src/theory/quantifiers/candidate_generator.cpp
@@ -130,21 +130,37 @@ Node CandidateGeneratorQE::getNextCandidate(){
CandidateGeneratorQELitEq::CandidateGeneratorQELitEq( QuantifiersEngine* qe, Node mpat ) :
d_match_pattern( mpat ), d_qe( qe ){
-
+ Assert( mpat.getKind()==EQUAL );
+ for( unsigned i=0; i<2; i++ ){
+ if( !quantifiers::TermDb::hasInstConstAttr(mpat[i]) ){
+ d_match_gterm = mpat[i];
+ }
+ }
}
void CandidateGeneratorQELitEq::resetInstantiationRound(){
}
void CandidateGeneratorQELitEq::reset( Node eqc ){
- d_eq = eq::EqClassesIterator( d_qe->getEqualityQuery()->getEngine() );
+ if( d_match_gterm.isNull() ){
+ d_eq = eq::EqClassesIterator( d_qe->getEqualityQuery()->getEngine() );
+ }else{
+ d_do_mgt = true;
+ }
}
Node CandidateGeneratorQELitEq::getNextCandidate(){
- while( !d_eq.isFinished() ){
- Node n = (*d_eq);
- ++d_eq;
- if( n.getType().isComparableTo( d_match_pattern[0].getType() ) ){
- //an equivalence class with the same type as the pattern, return reflexive equality
- return NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), n, n );
+ if( d_match_gterm.isNull() ){
+ while( !d_eq.isFinished() ){
+ Node n = (*d_eq);
+ ++d_eq;
+ if( n.getType().isComparableTo( d_match_pattern[0].getType() ) ){
+ //an equivalence class with the same type as the pattern, return reflexive equality
+ return NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), n, n );
+ }
+ }
+ }else{
+ if( d_do_mgt ){
+ d_do_mgt = false;
+ return NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), d_match_gterm, d_match_gterm );
}
}
return Node::null();
diff --git a/src/theory/quantifiers/candidate_generator.h b/src/theory/quantifiers/candidate_generator.h
index fb120dd08..d86891de7 100644
--- a/src/theory/quantifiers/candidate_generator.h
+++ b/src/theory/quantifiers/candidate_generator.h
@@ -108,6 +108,8 @@ private:
eq::EqClassesIterator d_eq;
//equality you are trying to match equalities for
Node d_match_pattern;
+ Node d_match_gterm;
+ bool d_do_mgt;
//einstantiator pointer
QuantifiersEngine* d_qe;
public:
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 621327c0b..111eab116 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -51,10 +51,12 @@ struct sortQuantifiersForSymbol {
struct sortTriggers {
bool operator() (Node i, Node j) {
- if( Trigger::isAtomicTrigger( i ) ){
- return i<j || !Trigger::isAtomicTrigger( j );
+ int wi = Trigger::getTriggerWeight( i );
+ int wj = Trigger::getTriggerWeight( j );
+ if( wi==wj ){
+ return i<j;
}else{
- return i<j && !Trigger::isAtomicTrigger( j );
+ return wi<wj;
}
}
};
@@ -257,19 +259,20 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
Node bd = d_quantEngine->getTermDatabase()->getInstConstantBody( f );
Trigger::collectPatTerms( d_quantEngine, f, bd, patTermsF, d_tr_strategy, d_user_no_gen[f], true );
Trace("auto-gen-trigger-debug") << "Collected pat terms for " << bd << ", no-patterns : " << d_user_no_gen[f].size() << std::endl;
- for( int i=0; i<(int)patTermsF.size(); i++ ){
- Trace("auto-gen-trigger-debug") << " " << patTermsF[i] << std::endl;
- }
- Trace("auto-gen-trigger-debug") << std::endl;
if( ntrivTriggers ){
sortTriggers st;
std::sort( patTermsF.begin(), patTermsF.end(), st );
}
+ for( unsigned i=0; i<patTermsF.size(); i++ ){
+ Trace("auto-gen-trigger-debug") << " " << patTermsF[i] << std::endl;
+ }
+ Trace("auto-gen-trigger-debug") << std::endl;
}
//sort into single/multi triggers
std::map< Node, std::vector< Node > > varContains;
std::map< Node, bool > vcMap;
std::map< Node, bool > rmPatTermsF;
+ int last_weight = -1;
for( unsigned i=0; i<patTermsF.size(); i++ ){
d_quantEngine->getTermDatabase()->getVarContainsNode( f, patTermsF[i], varContains[ patTermsF[i] ] );
bool newVar = false;
@@ -279,9 +282,12 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
newVar = true;
}
}
- if( ntrivTriggers && !newVar && !Trigger::isAtomicTrigger( patTermsF[i] ) ){
+ int curr_w = Trigger::getTriggerWeight( patTermsF[i] );
+ if( ntrivTriggers && !newVar && last_weight!=-1 && curr_w>last_weight ){
Trace("auto-gen-trigger-debug") << "Exclude expendible non-trivial trigger : " << patTermsF[i] << std::endl;
rmPatTermsF[patTermsF[i]] = true;
+ }else{
+ last_weight = curr_w;
}
}
for( std::map< Node, std::vector< Node > >::iterator it = varContains.begin(); it != varContains.end(); ++it ){
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index 0628b7fbc..48385e28b 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -242,7 +242,7 @@ bool Trigger::isUsable( Node n, Node q ){
}
Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) {
- Trace("trigger-debug") << "Is " << n << " a usable trigger?" << std::endl;
+ Trace("trigger-debug") << "Is " << n << " a usable trigger? pol/hasPol=" << pol << "/" << hasPol << std::endl;
if( n.getKind()==NOT ){
pol = !pol;
n = n[0];
@@ -254,7 +254,8 @@ Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) {
bool is_arith = n[0].getType().isReal();
for( unsigned i=0; i<2; i++) {
if( n[1-i].getKind()==INST_CONSTANT ){
- if( isUsableTrigger( n[i], f ) && !quantifiers::TermDb::containsTerm( n[i], n[1-i] ) && ( !do_negate || is_arith ) ){
+ if( ( ( isUsableTrigger( n[i], f ) && !quantifiers::TermDb::containsTerm( n[i], n[1-i] ) ) || !quantifiers::TermDb::hasInstConstAttr(n[i]) ) &&
+ ( !do_negate || is_arith ) ){
rtr = n;
break;
}
@@ -274,7 +275,7 @@ Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) {
Node veq;
if( QuantArith::isolate( it->first, m, veq, n.getKind() )!=0 ){
int vti = veq[0]==it->first ? 1 : 0;
- if( isUsableTrigger( veq[vti], f ) && !quantifiers::TermDb::containsTerm( veq[vti], veq[1-vti] ) ){
+ if( ( isUsableTrigger( veq[vti], f ) && !quantifiers::TermDb::containsTerm( veq[vti], veq[1-vti] ) ) || !quantifiers::TermDb::hasInstConstAttr(veq[vti]) ){
rtr = veq;
}
}
@@ -434,6 +435,23 @@ bool Trigger::isPureTheoryTrigger( Node n ) {
}
}
+int Trigger::getTriggerWeight( Node n ) {
+ if( isAtomicTrigger( n ) ){
+ return 0;
+ }else{
+ if( options::relationalTriggers() ){
+ if( n.getKind()==EQUAL || n.getKind()==IFF || n.getKind()==GEQ ){
+ for( unsigned i=0; i<2; i++ ){
+ if( n[i].getKind()==INST_CONSTANT && !quantifiers::TermDb::hasInstConstAttr( n[1-i] ) ){
+ return 0;
+ }
+ }
+ }
+ }
+ return 1;
+ }
+}
+
bool Trigger::isLocalTheoryExt( Node n, std::vector< Node >& vars, std::vector< Node >& patTerms ) {
if( !n.getType().isBoolean() && n.getKind()==APPLY_UF ){
if( std::find( patTerms.begin(), patTerms.end(), n )==patTerms.end() ){
diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h
index 11962008e..bbbf9495f 100644
--- a/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h
@@ -112,6 +112,7 @@ public:
static bool isSimpleTrigger( Node n );
static bool isBooleanTermTrigger( Node n );
static bool isPureTheoryTrigger( Node n );
+ static int getTriggerWeight( Node n );
static bool isLocalTheoryExt( Node n, std::vector< Node >& vars, std::vector< Node >& patTerms );
/** return data structure for producing matches for this trigger. */
static InstMatchGenerator* getInstMatchGenerator( Node q, Node n );
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 4be55ebb5..754b0c224 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -88,6 +88,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext*
d_te( te ),
d_lemmas_produced_c(u),
d_skolemized(u),
+ d_ierCounter_c(c),
//d_ierCounter(c),
//d_ierCounter_lc(c),
//d_ierCounterLastLc(c),
@@ -143,6 +144,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext*
d_total_inst_count_debug = 0;
//allow theory combination to go first, once initially
d_ierCounter = options::instWhenTcFirst() ? 0 : 1;
+ d_ierCounter_c = d_ierCounter;
d_ierCounter_lc = 0;
d_ierCounterLastLc = 0;
d_inst_when_phase = 1 + ( options::instWhenPhase()<1 ? 1 : options::instWhenPhase() );
@@ -375,6 +377,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
if( needsCheck ){
if( Trace.isOn("quant-engine-debug") ){
Trace("quant-engine-debug") << "Quantifiers Engine check, level = " << e << std::endl;
+ Trace("quant-engine-debug") << " depth : " << d_ierCounter_c << std::endl;
Trace("quant-engine-debug") << " modules to check : ";
for( unsigned i=0; i<qm.size(); i++ ){
Trace("quant-engine-debug") << qm[i]->identify() << " ";
@@ -470,6 +473,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
if( d_ierCounterLastLc!=d_ierCounter_lc || !options::instWhenStrictInterleave() || d_ierCounter%d_inst_when_phase!=0 ){
d_ierCounter = d_ierCounter + 1;
d_ierCounterLastLc = d_ierCounter_lc;
+ d_ierCounter_c = d_ierCounter_c.get() + 1;
}
}else if( e==Theory::EFFORT_LAST_CALL ){
d_ierCounter_lc = d_ierCounter_lc + 1;
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 228ac9ee9..920c45c1a 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -204,6 +204,7 @@ private:
std::map< Node, int > d_temp_inst_debug;
int d_total_inst_count_debug;
/** inst round counters TODO: make context-dependent? */
+ context::CDO< int > d_ierCounter_c;
int d_ierCounter;
int d_ierCounter_lc;
int d_ierCounterLastLc;
diff --git a/test/regress/regress0/push-pop/Makefile.am b/test/regress/regress0/push-pop/Makefile.am
index bcf6403b7..4bc16ea25 100644
--- a/test/regress/regress0/push-pop/Makefile.am
+++ b/test/regress/regress0/push-pop/Makefile.am
@@ -44,7 +44,8 @@ BUG_TESTS = \
bug-fmf-fun-skolem.smt2 \
bug674.smt2 \
inc-double-u.smt2 \
- fmf-fun-dbu.smt2
+ fmf-fun-dbu.smt2 \
+ inc-define.smt2
TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
diff --git a/test/regress/regress0/push-pop/inc-define.smt2 b/test/regress/regress0/push-pop/inc-define.smt2
new file mode 100644
index 000000000..27261eff6
--- /dev/null
+++ b/test/regress/regress0/push-pop/inc-define.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --incremental
+; EXPECT: sat
+; EXPECT: sat
+(set-logic QF_LIA)
+(declare-fun x () Int)
+(check-sat)
+(define t (not (= x 0)))
+(assert t)
+(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback