Enable --quant-cf by default. Fix bug in qcf for mixed Int/Real. Minor improvement to performance of E-matching.

7 files changed, 20 insertions, 5 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 577fa7413..c59d87d40 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1358,7 +1358,11 @@ void SmtEngine::setDefaults() {
       options::finiteModelFind.set( true );
     }
   }
-
+  if( options::finiteModelFind() ){
+    if( !options::quantConflictFind.wasSetByUser() ){
+      options::quantConflictFind.set( false );
+    }
+  }
   //until bugs 371,431 are fixed
   if( ! options::minisatUseElim.wasSetByUser()){
     if( d_logic.isQuantified() || options::produceModels() || options::produceAssignments() || options::checkModels() ){
diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index c78ea7b01..4a5197fc8 100644
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -36,6 +36,7 @@ InstMatchGenerator::InstMatchGenerator( Node pat ){
   Assert( quantifiers::TermDb::hasInstConstAttr(pat) );
   d_pattern = pat;
   d_match_pattern = pat;
+  d_match_pattern_type = pat.getType();
   d_next = NULL;
   d_matchPolicy = MATCH_GEN_DEFAULT;
 }
@@ -92,6 +93,7 @@ void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMat
         }
       }
     }
+    d_match_pattern_type = d_match_pattern.getType();
     Trace("inst-match-gen") << "Pattern is " << d_pattern << ", match pattern is " << d_match_pattern << std::endl;
     d_match_pattern_op = qe->getTermDatabase()->getOperator( d_match_pattern );
 
@@ -315,7 +317,7 @@ bool InstMatchGenerator::getNextMatch( Node f, InstMatch& m, QuantifiersEngine*
     t = d_cg->getNextCandidate();
     Trace("matching-debug2") << "Matching candidate : " << t << std::endl;
     //if t not null, try to fit it into match m
-    if( !t.isNull() && t.getType().isSubtypeOf( d_match_pattern.getType() ) ){
+    if( !t.isNull() && t.getType().isSubtypeOf( d_match_pattern_type ) ){
       success = getMatch( f, t, m, qe );
     }
   }while( !success && !t.isNull() );
@@ -675,6 +677,7 @@ InstMatchGeneratorSimple::InstMatchGeneratorSimple( Node f, Node pat ) : d_f( f
     if( d_match_pattern[i].getKind()==INST_CONSTANT ){
       d_var_num[i] = d_match_pattern[i].getAttribute(InstVarNumAttribute());
     }
+    d_match_pattern_arg_types.push_back( d_match_pattern[i].getType() );
   }
 }
 
@@ -713,7 +716,7 @@ void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngin
         Node t = it->first;
         Node prev = m.get( v );
         //using representatives, just check if equal
-        if( ( prev.isNull() || prev==t ) && t.getType().isSubtypeOf( d_match_pattern[argIndex].getType() ) ){
+        if( ( prev.isNull() || prev==t ) && t.getType().isSubtypeOf( d_match_pattern_arg_types[argIndex] ) ){
           m.setValue( v, t);
           addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) );
           m.setValue( v, prev);
diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h
index aa5d37713..850affe56 100644
--- a/src/theory/quantifiers/inst_match_generator.h
+++ b/src/theory/quantifiers/inst_match_generator.h
@@ -96,6 +96,8 @@ public:
   Node d_pattern;
   /** match pattern */
   Node d_match_pattern;
+  /** match pattern type */
+  TypeNode d_match_pattern_type;
   /** match pattern op */
   Node d_match_pattern_op;
 public:
@@ -204,6 +206,8 @@ private:
   Node d_f;
   /** match term */
   Node d_match_pattern;
+  /** match pattern arg types */
+  std::vector< TypeNode > d_match_pattern_arg_types;
   /** operator */
   Node d_op;
   /** to indicies */
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 8cb693117..97a43a96d 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -143,7 +143,7 @@ option fmfBoundIntLazy --fmf-bound-int-lazy bool :default false :read-write
 option axiomInstMode --axiom-inst=MODE CVC4::theory::quantifiers::AxiomInstMode :default CVC4::theory::quantifiers::AXIOM_INST_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToAxiomInstMode :handler-include "theory/quantifiers/options_handlers.h"
  policy for instantiating axioms
 
-option quantConflictFind --quant-cf bool :read-write :default false
+option quantConflictFind --quant-cf bool :read-write :default true
  enable conflict find mechanism for quantifiers
 option qcfMode --quant-cf-mode=MODE CVC4::theory::quantifiers::QcfMode :default CVC4::theory::quantifiers::QCF_PROP_EQ :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToQcfMode :handler-include "theory/quantifiers/options_handlers.h"
  what effort to apply conflict find mechanism
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index f976a0dbf..d58ce14b1 100755
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -43,6 +43,7 @@ void QuantInfo::initialize( Node q, Node qn ) {
   for( unsigned i=0; i<q[0].getNumChildren(); i++ ){

     d_var_num[q[0][i]] = i;

     d_vars.push_back( q[0][i] );

+    d_var_types.push_back( q[0][i].getType() );

   }

 

   registerNode( qn, true, true );

@@ -145,6 +146,7 @@ void QuantInfo::flatten( Node n, bool beneathQuant ) {
       Trace("qcf-qregister-debug2") << "Add FLATTEN VAR : " << n << std::endl;

       d_var_num[n] = d_vars.size();

       d_vars.push_back( n );

+      d_var_types.push_back( n.getType() );

       d_match.push_back( TNode::null() );

       d_match_term.push_back( TNode::null() );

       if( n.getKind()==ITE ){

@@ -1524,7 +1526,7 @@ bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) {
               if( it != d_qn[index]->d_data.end() ) {

                 d_qni.push_back( it );

                 //set the match

-                if( qi->setMatch( p, d_qni_bound[index], it->first ) ){

+                if( it->first.getType().isSubtypeOf( qi->d_var_types[repVar] ) && qi->setMatch( p, d_qni_bound[index], it->first ) ){

                   Debug("qcf-match-debug") << "       Binding variable" << std::endl;

                   if( d_qn.size()<d_qni_size ){

                     d_qn.push_back( &it->second );

diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index 93e1f72a6..b2dc680f2 100755
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -118,6 +118,7 @@ public:
   QuantInfo() : d_mg( NULL ) {}

   ~QuantInfo() { delete d_mg; }

   std::vector< TNode > d_vars;

+  std::vector< TypeNode > d_var_types;

   std::map< TNode, int > d_var_num;

   std::vector< int > d_tsym_vars;

   std::map< TNode, bool > d_inMatchConstraint;

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 46995653f..eabba85bf 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -524,6 +524,7 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std
     for( int i=0; i<(int)terms.size(); i++ ){
       Trace("inst") << "   " << terms[i];
       Trace("inst") << std::endl;
+      Assert( terms[i].getType().isSubtypeOf( f[0][i].getType() ) );
     }
     if( options::cbqi() ){
       for( int i=0; i<(int)terms.size(); i++ ){