summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/smt/smt_engine.cpp21
-rw-r--r--src/theory/datatypes/theory_datatypes.cpp20
-rw-r--r--src/theory/quantifiers/inst_match_generator.cpp33
-rw-r--r--src/theory/quantifiers/options10
-rw-r--r--src/theory/quantifiers_engine.cpp1
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback