On-demand upper bound lemmas for deltas in quantified LRA (for casc). Force no macros...

diff --git a/contrib/run-script-casc25-tfn b/contrib/run-script-casc25-tfn
index d3c5d0344630a9a93d1ebf10f49b971ac9e98b52..6888d7b496bc6ef63d60e186286832a20300afe5 100644 (file)
--- a/contrib/run-script-casc25-tfn
+++ b/contrib/run-script-casc25-tfn
@@ -15,7 +15,7 @@ echo "------- cvc4-tfn casc 25 : $bench at $2..."
 function trywith {
   limit=$1; shift;
   echo "--- Run $@ at $limit...";
-  (ulimit -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive "$@" $bench) 2>/dev/null |
+  (ulimit -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive --force-logic="UFNIRA" "$@" $bench) 2>/dev/null |
   (read w1 w2 w3 result w4 w5;
   case "$result" in
   Satisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
@@ -25,11 +25,10 @@ function trywith {
 }
 function finishwith {
   echo "--- Run $@...";
-  $cvc4 --lang=tptp --no-checking --no-interactive "$@" $bench
+  $cvc4 --lang=tptp --no-checking --no-interactive --force-logic="UFNIRA" "$@" $bench
 }
 
 trywith 30 --cbqi2 --decision=internal --full-saturate-quant
-trywith 60 --finite-model-find --sort-inference --uf-ss-fair
 trywith 30 --cbqi --full-saturate-quant
 trywith 60 --cbqi --cbqi-recurse --full-saturate-quant
 trywith 60 --fmf-bound-int --macros-quant

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 6fdfadbd351afa8124e37f76d6531e955485fa1e..54c97750aacd1628723cb4a1aff626e6a5b5faf4 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3272,7 +3272,7 @@ void SmtEnginePrivate::processAssertions() {
       }
     }
     dumpAssertions("post-skolem-quant", d_assertions);
-    if( options::macrosQuant() ){
+    if( options::macrosQuant() && !options::incrementalSolving() ){
       //quantifiers macro expansion
       bool success;
       do{

diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index 22ffcd278008d851f7b5ddd71a998a54352e1bd3..8e7e3d69cce066862921613d5f7723febf7bf826 100644 (file)
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -706,7 +706,7 @@ void CegInstantiator::getDeltaLemmas( std::vector< Node >& lems ) {
   */
 }
 
-void CegInstantiator::check() {
+bool CegInstantiator::check() {
 
   for( unsigned r=0; r<2; r++ ){
     std::vector< Node > subs;
@@ -716,10 +716,11 @@ void CegInstantiator::check() {
     std::vector< int > subs_typ;
     //try to add an instantiation
     if( addInstantiation( subs, vars, coeff, has_coeff, subs_typ, 0, r==0 ? 0 : 2 ) ){
-      return;
+      return true;
     }
   }
   Trace("cegqi-engine") << "  WARNING : unable to find CEGQI single invocation instantiation." << std::endl;
+  return false;
 }
 
 

diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h
index 54f762720b8ea2fd9dca4c0ef231e69ccacf2d4f..eb99fc4f66b41c887f2165456ca08d4f59aa6b30 100644 (file)
--- a/src/theory/quantifiers/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/ce_guided_single_inv.h
@@ -72,7 +72,7 @@ public:
   //delta
   Node d_n_delta;
   //check : add instantiations based on valuation of d_vars
-  void check();
+  bool check();
   // get delta lemmas : on-demand force minimality of d_n_delta
   void getDeltaLemmas( std::vector< Node >& lems );
 };

diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index fdb64f6b0c56ada26525c4bfbd5942150e7dbc24..da3c0cce072658893cf8970afc4aaeb79dbedd40 100644 (file)
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -1717,15 +1717,18 @@ void TermGenEnv::collectSignatureInformation() {
   for( std::map< Node, TermArgTrie >::iterator it = getTermDatabase()->d_func_map_trie.begin(); it != getTermDatabase()->d_func_map_trie.end(); ++it ){
     if( !getTermDatabase()->d_op_map[it->first].empty() ){
       Node nn = getTermDatabase()->d_op_map[it->first][0];
+      Trace("sg-rel-sig-debug") << "Check in signature : " << nn << std::endl;
       if( d_cg->isHandledTerm( nn ) && nn.getKind()!=APPLY_SELECTOR_TOTAL && !nn.getType().isBoolean() ){
         bool do_enum = true;
         //check if we have enumerated ground terms
         if( nn.getKind()==APPLY_UF ){
+          Trace("sg-rel-sig-debug") << "Check enumeration..." << std::endl;
           if( !d_cg->hasEnumeratedUf( nn ) ){
             do_enum = false;
           }
         }
         if( do_enum ){
+          Trace("sg-rel-sig-debug") << "Set enumeration..." << std::endl;
           d_funcs.push_back( it->first );
           for( unsigned i=0; i<nn.getNumChildren(); i++ ){
             d_func_args[it->first].push_back( nn[i].getType() );
@@ -1738,6 +1741,7 @@ void TermGenEnv::collectSignatureInformation() {
           getTermDatabase()->computeUfEqcTerms( it->first );
         }
       }
+      Trace("sg-rel-sig-debug") << "Done check in signature : " << nn << std::endl;
     }
   }
   //shuffle functions

diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index cbf0dbbd9a1d916431763cdc7963f9e412041438..de80146f9ffbb3a4cc8ce8de9b35ca8866a60e6b 100644 (file)
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -369,6 +369,7 @@ InstStrategyCegqi::InstStrategyCegqi( QuantifiersEngine * qe ) : InstStrategy( q
 
 void InstStrategyCegqi::processResetInstantiationRound( Theory::Effort effort ) {
   d_check_delta_lemma = true;
+  d_check_delta_lemma_lc = true;
 }
 
 int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) {
@@ -383,6 +384,9 @@ int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) {
         d_n_delta = NodeManager::currentNM()->mkSkolem( "delta", NodeManager::currentNM()->realType(), "delta for cegqi inst strategy" );
         Node delta_lem = NodeManager::currentNM()->mkNode( GT, d_n_delta, NodeManager::currentNM()->mkConst( Rational( 0 ) ) );
         d_quantEngine->getOutputChannel().lemma( delta_lem );
+        d_n_delta_ub = NodeManager::currentNM()->mkConst( Rational(1)/Rational(1000000) );
+        Node delta_lem_ub = NodeManager::currentNM()->mkNode( LT, d_n_delta, d_n_delta_ub );
+        d_quantEngine->getOutputChannel().lemma( delta_lem_ub );
       }
       cinst->d_n_delta = d_n_delta;
       for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
@@ -412,8 +416,18 @@ int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) {
     }
     Trace("inst-alg") << "-> Run cegqi for " << f << std::endl;
     d_curr_quant = f;
-    cinst->check();
+    bool addedLemma = cinst->check();
     d_curr_quant = Node::null();
+    return addedLemma ? STATUS_UNKNOWN : STATUS_UNFINISHED;
+  }else if( e==3 ){
+    if( d_check_delta_lemma_lc ){
+      d_check_delta_lemma_lc = false;
+      d_n_delta_ub = NodeManager::currentNM()->mkNode( MULT, d_n_delta_ub, d_n_delta_ub );
+      d_n_delta_ub = Rewriter::rewrite( d_n_delta_ub );
+      Trace("cegqi") << "Delta lemma for " << d_n_delta_ub << std::endl;
+      Node delta_lem_ub = NodeManager::currentNM()->mkNode( LT, d_n_delta, d_n_delta_ub );
+      d_quantEngine->getOutputChannel().lemma( delta_lem_ub );
+    }
   }
   return STATUS_UNKNOWN;
 }

diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index 586cd492cad796760b27da827aa563329ec634c7..13e8cf54b07f726000a6e394a488a31bc62d5cd5 100644 (file)
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -100,8 +100,10 @@ private:
   CegqiOutputInstStrategy * d_out;
   std::map< Node, CegInstantiator * > d_cinst;
   Node d_n_delta;
+  Node d_n_delta_ub;
   Node d_curr_quant;
   bool d_check_delta_lemma;
+  bool d_check_delta_lemma_lc;
   /** process functions */
   void processResetInstantiationRound( Theory::Effort effort );
   int process( Node f, Theory::Effort effort, int e );

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 8c99881d65367b3ad806eb7f2a75c85a7a355a10..1898664944b5862ce20bebd0a16d82819799d279 100644 (file)
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -945,6 +945,7 @@ Node TermDb::getSkolemizedBody( Node f ){
 }
 
 Node TermDb::getEnumerateTerm( TypeNode tn, unsigned index ) {
+  Trace("term-db-enum") << "Get enumerate term " << tn << " " << index << std::endl;
   std::map< TypeNode, unsigned >::iterator it = d_typ_enum_map.find( tn );
   unsigned teIndex;
   if( it==d_typ_enum_map.end() ){