Enable --quant-cf by default. Fix bug in qcf for mixed Int/Real. Minor improvement...

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 577fa7413deaa2113045d6fb60a94575a7668d4f..c59d87d40a6fa4a163064557e9088ccb6ee19c5c 100644 (file)
--- 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 c78ea7b013ae4400799ebebef6d2219cb2a183aa..4a5197fc895d2ad2d6a92ce3e93e332ff53d02cd 100644 (file)
--- 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 aa5d377132c06fd1094172e8b0512d9255870b4d..850affe56a4aff30b1d4e26c913fbd84d8002e1b 100644 (file)
--- 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 8cb693117762e5299ed9e51fcd630d7bef32140d..97a43a96dbb81438dcbbaab8903c66eece79d585 100644 (file)
--- 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 f976a0dbf30863a4c974ab6028693e67b6e04a91..d58ce14b16975fd0eb754961fd3cc57fb03771e5 100755 (executable)
--- 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++ ){\r
     d_var_num[q[0][i]] = i;\r
     d_vars.push_back( q[0][i] );\r
+    d_var_types.push_back( q[0][i].getType() );\r
   }\r
 \r
   registerNode( qn, true, true );\r
@@ -145,6 +146,7 @@ void QuantInfo::flatten( Node n, bool beneathQuant ) {
       Trace("qcf-qregister-debug2") << "Add FLATTEN VAR : " << n << std::endl;\r
       d_var_num[n] = d_vars.size();\r
       d_vars.push_back( n );\r
+      d_var_types.push_back( n.getType() );\r
       d_match.push_back( TNode::null() );\r
       d_match_term.push_back( TNode::null() );\r
       if( n.getKind()==ITE ){\r
@@ -1524,7 +1526,7 @@ bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) {
               if( it != d_qn[index]->d_data.end() ) {\r
                 d_qni.push_back( it );\r
                 //set the match\r
-                if( qi->setMatch( p, d_qni_bound[index], it->first ) ){\r
+                if( it->first.getType().isSubtypeOf( qi->d_var_types[repVar] ) && qi->setMatch( p, d_qni_bound[index], it->first ) ){\r
                   Debug("qcf-match-debug") << "       Binding variable" << std::endl;\r
                   if( d_qn.size()<d_qni_size ){\r
                     d_qn.push_back( &it->second );\r

diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index 93e1f72a66a7548ae1e7ff7fb4aea545d489250d..b2dc680f22742af990988a76cd61a306167ca262 100755 (executable)
--- 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 ) {}\r
   ~QuantInfo() { delete d_mg; }\r
   std::vector< TNode > d_vars;\r
+  std::vector< TypeNode > d_var_types;\r
   std::map< TNode, int > d_var_num;\r
   std::vector< int > d_tsym_vars;\r
   std::map< TNode, bool > d_inMatchConstraint;\r

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 46995653fa1d516db0ff3b18103dcc74e405ce68..eabba85bfa0c65da2e28d7a2865e25b89e904cdf 100644 (file)
--- 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++ ){