Bug fixes for --purify-triggers, --dt-force-assignment.

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 98ae6d3ce402a71c3e19099e91666acc09cd8ef1..220318b4c7a23684c3495e025bacb589705a9eed 100644 (file)
--- 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 65d307a34dcccd0e647922d963ffcb134a021d80..7015b772e4c222bd1cc42dd30e81ede7bc17bc20 100644 (file)
--- 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 6dbe1ec4246a5633d418c6b2ba3dac5f4627440b..ad71e60ef0d44435323f73ebffebb0f7987adeff 100644 (file)
--- 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 f33f1ce839ac7edee96ed26683b175ef4c7b0513..5ef7e9efa8578d5aa726372e426711d7dea2c678 100644 (file)
--- 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 03143ab9caa906ab29efc71b0efc5dd42ccc9700..d6bd8e574e4a799e3332347f9445d4e65d075da2 100644 (file)
--- 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;