From 34a27e2fef540ee3d90c43f771397e0e9ce3fef9 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 26 Aug 2014 14:29:29 +0200 Subject: [PATCH] Bug fixes for --purify-triggers, --dt-force-assignment. --- src/smt/smt_engine.cpp | 21 ++++++++---- src/theory/datatypes/theory_datatypes.cpp | 20 ++++++----- .../quantifiers/inst_match_generator.cpp | 33 +++++++++++-------- src/theory/quantifiers/options | 10 +++--- src/theory/quantifiers_engine.cpp | 1 + 5 files changed, 52 insertions(+), 33 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 98ae6d3ce..220318b4c 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1290,6 +1290,20 @@ void SmtEngine::setDefaults() { if( options::qcfMode.wasSetByUser() || options::qcfTConstraint() ){ options::quantConflictFind.set( true ); } + //for induction techniques + if( options::quantInduction() ){ + if( !options::dtStcInduction.wasSetByUser() ){ + options::dtStcInduction.set( true ); + } + if( !options::intWfInduction.wasSetByUser() ){ + options::intWfInduction.set( true ); + } + } + if( options::intWfInduction() ){ + if( !options::purifyTriggers.wasSetByUser() ){ + options::purifyTriggers.set( true ); + } + } //until bugs 371,431 are fixed if( ! options::minisatUseElim.wasSetByUser()){ @@ -1339,13 +1353,6 @@ void SmtEngine::setDefaults() { Warning() << "SmtEngine: turning off incremental solving mode (not yet supported with --proof" << endl; setOption("incremental", SExpr("false")); } - - // datatypes theory should assign values to all datatypes terms if logic is quantified - if (d_logic.isQuantified() && d_logic.isTheoryEnabled(THEORY_DATATYPES)) { - if( !options::dtForceAssignment.wasSetByUser() ){ - options::dtForceAssignment.set(true); - } - } } void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 65d307a34..7015b772e 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -190,19 +190,23 @@ void TheoryDatatypes::check(Effort e) { } } } - /* - if( !needSplit && mustSpecifyAssignment() ){ + + if( !needSplit && options::dtForceAssignment() ){ //for the sake of termination, we must choose the constructor of a ground term //NEED GUARENTEE: groundTerm should not contain any subterms of the same type // TODO: this is probably not good enough, actually need fair enumeration strategy - Node groundTerm = n.getType().mkGroundTerm(); - int index = Datatype::indexOf( groundTerm.getOperator().toExpr() ); - if( pcons[index] ){ - consIndex = index; + if( !n.getType().isRecord() ){ //FIXME + Node groundTerm = n.getType().mkGroundTerm(); + if( groundTerm.getOperator().getType().isConstructor() ){ //FIXME + int index = Datatype::indexOf( groundTerm.getOperator().toExpr() ); + if( pcons[index] ){ + consIndex = index; + } + needSplit = true; + } } - needSplit = true; } - */ + if( needSplit && consIndex!=-1 ) { //if only one constructor, then this term must be this constructor if( dt.getNumConstructors()==1 ){ diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index 6dbe1ec42..ad71e60ef 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -235,8 +235,7 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi //now, fit children into match //we will be requesting candidates for matching terms for each child for( int i=0; i<(int)d_children.size(); i++ ){ - Node rep = q->getRepresentative( t[ d_children_index[i] ] ); - d_children[i]->reset( rep, qe ); + d_children[i]->reset( t[ d_children_index[i] ], qe ); } success = continueNextMatch( f, m, qe ); } @@ -277,6 +276,7 @@ void InstMatchGenerator::resetInstantiationRound( QuantifiersEngine* qe ){ } void InstMatchGenerator::reset( Node eqc, QuantifiersEngine* qe ){ + eqc = qe->getEqualityQuery()->getRepresentative( eqc ); Trace("matching-debug2") << this << " reset " << eqc << "." << std::endl; if( !eqc.isNull() ){ d_eq_class = eqc; @@ -400,14 +400,16 @@ bool VarMatchGeneratorBooleanTerm::getNextMatch( Node f, InstMatch& m, Quantifie if( !m.set( qe, d_var_num[0], s ) ){ return false; }else{ - return continueNextMatch( f, m, qe ); - } - }else{ - if( d_rm_prev ){ - m.d_vals[d_var_num[0]] = Node::null(); + if( continueNextMatch( f, m, qe ) ){ + return true; + } } - return false; } + if( d_rm_prev ){ + m.d_vals[d_var_num[0]] = Node::null(); + d_rm_prev = false; + } + return false; } VarMatchGeneratorTermSubs::VarMatchGeneratorTermSubs( Node var, Node subs ) : @@ -419,20 +421,23 @@ bool VarMatchGeneratorTermSubs::getNextMatch( Node f, InstMatch& m, QuantifiersE if( !d_eq_class.isNull() ){ Trace("var-trigger-matching") << "Matching " << d_eq_class << " against " << d_var << " in " << d_subs << std::endl; Node s = d_subs.substitute( d_var, d_eq_class ); + s = Rewriter::rewrite( s ); Trace("var-trigger-matching") << "...got " << s << std::endl; d_eq_class = Node::null(); d_rm_prev = m.get( d_var_num[0] ).isNull(); if( !m.set( qe, d_var_num[0], s ) ){ return false; }else{ - return continueNextMatch( f, m, qe ); - } - }else{ - if( d_rm_prev ){ - m.d_vals[d_var_num[0]] = Node::null(); + if( continueNextMatch( f, m, qe ) ){ + return true; + } } - return false; } + if( d_rm_prev ){ + m.d_vals[d_var_num[0]] = Node::null(); + d_rm_prev = false; + } + return false; } /** constructors */ diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index f33f1ce83..5ef7e9efa 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -63,7 +63,7 @@ option relevantTriggers --relevant-triggers bool :default false prefer triggers that are more relevant based on SInE style analysis option relationalTriggers --relational-triggers bool :default false choose relational triggers such as x = f(y), x >= f(y) -option purifyTriggers --purify-triggers bool :default false +option purifyTriggers --purify-triggers bool :default false :read-write purify triggers, e.g. f( x+1 ) becomes f( y ), x mapsto y-1 option triggerSelMode --trigger-sel CVC4::theory::quantifiers::TriggerSelMode :default CVC4::theory::quantifiers::TRIGGER_SEL_DEFAULT :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToTriggerSelMode :handler-include "theory/quantifiers/options_handlers.h" selection mode for triggers @@ -148,11 +148,13 @@ option quantRewriteRules --rewrite-rules bool :default true option rrOneInstPerRound --rr-one-inst-per-round bool :default false add one instance of rewrite rule per round -option dtStcInduction --dt-stc-ind bool :default false +option quantInduction --quant-ind bool :default false + use all available techniques for inductive reasoning +option dtStcInduction --dt-stc-ind bool :read-write :default false apply strengthening for existential quantification over datatypes based on structural induction -option intWfInduction --int-wf-ind bool :default false +option intWfInduction --int-wf-ind bool :read-write :default false apply strengthening for integers based on well-founded induction -option conjectureGen --conjecture-gen bool :default false +option conjectureGen --conjecture-gen bool :read-write :default false generate candidate conjectures for inductive proofs endmodule diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 03143ab9c..d6bd8e574 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -382,6 +382,7 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std Assert( f.getKind()==FORALL ); Assert( vars.size()==terms.size() ); Node body = getInstantiation( f, vars, terms ); + Trace("inst-assert") << "(assert " << body << ")" << std::endl; //make the lemma NodeBuilder<> nb(kind::OR); nb << f.notNode() << body; -- 2.30.2