Minor improvements to infrastructure. Minor changes to default options. Add tff scrip...

diff --git a/contrib/run-script-casc25-fnt b/contrib/run-script-casc25-fnt
index c53a0f26d0ce334cf9847570eda5bd3ddb54c999..7f007186ca192813b917074f150b694c7dcd693c 100644 (file)
--- a/contrib/run-script-casc25-fnt
+++ b/contrib/run-script-casc25-fnt
@@ -29,10 +29,10 @@ function finishwith {
 }
 
 # designed for 300 seconds
-trywith 30 --finite-model-find --sort-inference --uf-ss-fair --mbqi=abs
+trywith 30 --finite-model-find --fmf-inst-engine --sort-inference --uf-ss-fair --mbqi=gen-ev
 trywith 20 --finite-model-find --uf-ss=no-minimal --sort-inference --uf-ss-fair
-trywith 20 --finite-model-find --decision=internal
+trywith 20 --finite-model-find --decision=internal --sort-inference --uf-ss-fair
 trywith 20 --finite-model-find --uf-ss-totality --sort-inference --uf-ss-fair --mbqi=gen-ev
-trywith 60 --finite-model-find --fmf-inst-engine --sort-inference --uf-ss-fair --mbqi=gen-ev
-finishwith --finite-model-find --quant-cf --sort-inference --uf-ss-fair --mbqi=abs
+trywith 60 --finite-model-find --quant-cf --sort-inference --uf-ss-fair --mbqi=abs
+finishwith --finite-model-find --sort-inference --uf-ss-fair --mbqi=abs
 # echo "% SZS status" "GaveUp for $filename"

diff --git a/contrib/run-script-casc25-fof b/contrib/run-script-casc25-fof
index 3986b42f664662ed487d0a6cb77c2d9d83ad31b2..b6bea37dd539dbc426c1eca76afefe7ebf4dfea4 100755 (executable)
--- a/contrib/run-script-casc25-fof
+++ b/contrib/run-script-casc25-fof
@@ -33,13 +33,13 @@ trywith 15 --relevant-triggers --clause-split --full-saturate-quant
 trywith 15 --clause-split --no-e-matching --full-saturate-quant 
 trywith 15 --finite-model-find --quant-cf --sort-inference --uf-ss-fair
 trywith 5 --trigger-sel=max --full-saturate-quant
-trywith 5 --multi-trigger-when-single --full-saturate-quant 
+trywith 5 --relevant-triggers --clause-split --multi-trigger-when-single --full-saturate-quant 
 trywith 5 --multi-trigger-when-single --multi-trigger-priority --full-saturate-quant 
 trywith 5 --pre-skolem-quant --no-pre-skolem-quant-nested --full-saturate-quant
-trywith 15 --decision=internal --full-saturate-quant
-trywith 15 --no-quant-cf --full-saturate-quant
-trywith 15 --trigger-sel=min --full-saturate-quant
-trywith 30 --prenex-quant=none --full-saturate-quant
+trywith 15 --relevant-triggers --decision=internal --full-saturate-quant
+trywith 15 --clause-split --no-quant-cf --full-saturate-quant
+trywith 15 --clause-split --trigger-sel=min --full-saturate-quant
+trywith 30 --relevant-triggers --prenex-quant=none --full-saturate-quant
 trywith 30 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant
 trywith 30 --finite-model-find --fmf-inst-engine --sort-inference --uf-ss-fair --mbqi=gen-ev
 finishwith --term-db-mode=relevant --full-saturate-quant

diff --git a/contrib/run-script-casc25-tff b/contrib/run-script-casc25-tff
new file mode 100644 (file)
index 0000000..f6d244a
--- /dev/null
+++ b/contrib/run-script-casc25-tff
@@ -0,0 +1,38 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+file=${bench##*/}
+filename=${file%.*}
+
+echo "------- cvc4-tff casc 25 : $bench at $2..."
+
+# use: trywith [params..]
+# to attempt a run.  If an SZS ontology result is printed, then
+# the run script terminates immediately.  Otherwise, this
+# function returns normally.
+function trywith {
+  limit=$1; shift;
+  echo "--- Run $@ at $limit...";
+  (ulimit -t "$limit";$cvc4 --lang=tptp --no-checking --no-interactive "$@" $bench) 2>/dev/null |
+  (read w1 w2 w3 result w4 w5;
+  case "$result" in
+  Unsatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  Theorem) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
+  esac; exit 1)
+  if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+}
+function finishwith {
+  echo "--- Run $@...";
+  $cvc4 --lang=tptp --no-checking --no-interactive "$@" $bench
+}
+
+trywith 10 --cbqi2 --decision=internal --full-saturate-quant --force-logic="UFNIRA"
+trywith 10 --relevant-triggers --full-saturate-quant --force-logic="UFNIRA"
+trywith 20 --cbqi --cbqi-recurse --full-saturate-quant --force-logic="UFNIRA"
+trywith 20 --no-e-matching --full-saturate-quant --force-logic="UFNIRA"
+trywith 20 --qcf-tconstraint --full-saturate-quant --force-logic="UFNIRA"
+trywith 70 --full-saturate-quant --force-logic="UFNIRA"
+finishwith --cbqi2 --cbqi-recurse --full-saturate-quant --force-logic="UFNIRA"
+# echo "% SZS status" "GaveUp for $filename"

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 6267a645ecc3d7580fe6d4d4a150a86e51034943..b20b8469045d4c7cc5100da33f2883cc7dce1974 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1430,6 +1430,9 @@ void SmtEngine::setDefaults() {
     if( !options::quantConflictFind.wasSetByUser() ){
       options::quantConflictFind.set( false );
     }
+    if( !options::instNoEntail.wasSetByUser() ){
+      options::instNoEntail.set( false );
+    }
   }
 
   //implied options...

diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index e1fc9e793e0e567ab660a56bad01605afe790661..5e6bcf0b4dd0f5f6f71da142a6c65404df639d15 100644 (file)
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -138,8 +138,8 @@ bool CegInstantiation::needsCheck( Theory::Effort e ) {
   return e>=Theory::EFFORT_LAST_CALL;
 }
 
-bool CegInstantiation::needsModel( Theory::Effort e ) {
-  return true;
+unsigned CegInstantiation::needsModel( Theory::Effort e ) {
+  return QuantifiersEngine::QEFFORT_MODEL;  
 }
 
 void CegInstantiation::check( Theory::Effort e, unsigned quant_e ) {
@@ -543,8 +543,11 @@ void CegInstantiation::printSygusTerm( std::ostream& out, Node n ) {
       }
       return;
     }
+  }else if( !n.getAttribute(SygusProxyAttribute()).isNull() ){
+    out << n.getAttribute(SygusProxyAttribute());
+  }else{
+    out << n;
   }
-  out << n;
 }
 
 void CegInstantiation::collectDisjuncts( Node n, std::vector< Node >& d ) {

diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h
index f5077ad04f0da9d3a7ce287824b5fd14fc81e85a..52e1107207b47a56731179527e6e3123bb20cd95 100644 (file)
--- a/src/theory/quantifiers/ce_guided_instantiation.h
+++ b/src/theory/quantifiers/ce_guided_instantiation.h
@@ -118,7 +118,7 @@ public:
   CegInstantiation( QuantifiersEngine * qe, context::Context* c );
 public:
   bool needsCheck( Theory::Effort e );
-  bool needsModel( Theory::Effort e );
+  unsigned needsModel( Theory::Effort e );
   /* Call during quantifier engine's check */
   void check( Theory::Effort e, unsigned quant_e );
   /* Called for new quantifiers */

diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 6e73b37a79a4560ecece3c5bde911e4cf9ff5ac7..1d6676464886394b49d6d5f1b384e5dbdbad9dd4 100644 (file)
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -51,8 +51,8 @@ bool ModelEngine::needsCheck( Theory::Effort e ) {
   return e==Theory::EFFORT_LAST_CALL;
 }
 
-bool ModelEngine::needsModel( Theory::Effort e ) {
-  return true;  
+unsigned ModelEngine::needsModel( Theory::Effort e ) {
+  return QuantifiersEngine::QEFFORT_MODEL;  
 }
 
 void ModelEngine::check( Theory::Effort e, unsigned quant_e ){

diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h
index 8c53084f0c00ea11c187ae97758a510fcbca7f01..6cdb47be2f7d77d29fc6d3c69212fe3e214131b0 100644 (file)
--- a/src/theory/quantifiers/model_engine.h
+++ b/src/theory/quantifiers/model_engine.h
@@ -48,7 +48,7 @@ public:
   virtual ~ModelEngine();
 public:
   bool needsCheck( Theory::Effort e );
-  bool needsModel( Theory::Effort e );
+  unsigned needsModel( Theory::Effort e );
   void check( Theory::Effort e, unsigned quant_e );
   void registerQuantifier( Node f );
   void assertNode( Node f );

diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index a529e37d034675cf73d2444d6764f6202d635179..4541c3d8a05aa034104b95d1c4adf29e4624df24 100644 (file)
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -166,7 +166,7 @@ option instNoEntail --inst-no-entail bool :read-write :default true
  
 ### rewrite rules options 
  
-option quantRewriteRules --rewrite-rules bool :default true
+option quantRewriteRules --rewrite-rules bool :default false
  use rewrite rules module
 option rrOneInstPerRound --rr-one-inst-per-round bool :default false
  add one instance of rewrite rule per round
@@ -207,6 +207,8 @@ option cegqiSingleInv --cegqi-si bool :default false
   process single invocation synthesis conjectures
 option cegqiSingleInvReconstruct --cegqi-si-reconstruct bool :default true
   reconstruct solutions for single invocation conjectures in original grammar
+option cegqiSingleInvReconstructConst --cegqi-si-reconstruct-const bool :default true
+  include constants when reconstruct solutions for single invocation conjectures in original grammar
 option cegqiSingleInvAbort --cegqi-si-abort bool :default false
   abort if our synthesis conjecture is not single invocation
   

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index e6f1ceee05f208a76d8e20874870a6639758466c..6c32ccb4a66588e2f34460d26f7e7024608c4231 100644 (file)
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1591,8 +1591,12 @@ Node TermDbSygus::builtinToSygusConst( Node c, TypeNode tn ) {
       sc = Node::fromExpr( dt[carg].getSygusOp() );
     }else{
       //TODO
-      
-      
+      if( !options::cegqiSingleInvReconstructConst() ){
+        Node k = NodeManager::currentNM()->mkSkolem( "sy", tn, "sygus proxy" );
+        SygusProxyAttribute spa;
+        k.setAttribute(spa,c);
+        sc = k;
+      }
     }
     d_builtin_const_to_sygus[tn][c] = sc;
     return sc;

diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index db84ba885fc4528b44feeb334ca25c7dbe230d36..37b1528b3d0ea9362f95f657365a1832e93a63f3 100644 (file)
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -88,6 +88,10 @@ typedef expr::Attribute<RrPriorityAttributeId, uint64_t> RrPriorityAttribute;
 struct LtePartialInstAttributeId {};
 typedef expr::Attribute< LtePartialInstAttributeId, bool > LtePartialInstAttribute;
 
+// attribute for "contains instantiation constants from"
+struct SygusProxyAttributeId {};
+typedef expr::Attribute<SygusProxyAttributeId, Node> SygusProxyAttribute;
+
 class QuantifiersEngine;
 
 namespace inst{

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index f6645c493f2872f6b64f22b5df08ff760a6341e2..19e39d5b55a86152a0395de6d7ed78b8ea0e2722 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -44,6 +44,9 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::inst;
 
+unsigned QuantifiersModule::needsModel( Theory::Effort e ) {
+  return QuantifiersEngine::QEFFORT_NONE;  
+}
 
 eq::EqualityEngine * QuantifiersModule::getEqualityEngine() {
   return d_quantEngine->getMasterEqualityEngine();
@@ -266,7 +269,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
     d_ierCounter_lc++;
   }
   bool needsCheck = !d_lemmas_waiting.empty();
-  bool needsModel = false;
+  unsigned needsModelE = QEFFORT_NONE;
   std::vector< QuantifiersModule* > qm;
   if( d_model->checkNeeded() ){
     needsCheck = needsCheck || e>=Theory::EFFORT_LAST_CALL;  //always need to check at or above last call
@@ -274,9 +277,8 @@ void QuantifiersEngine::check( Theory::Effort e ){
       if( d_modules[i]->needsCheck( e ) ){
         qm.push_back( d_modules[i] );
         needsCheck = true;
-        if( d_modules[i]->needsModel( e ) ){
-          needsModel = true;
-        }
+        unsigned me = d_modules[i]->needsModel( e );
+        needsModelE = me<needsModelE ? me : needsModelE;
       }
     }
   }
@@ -336,12 +338,11 @@ void QuantifiersEngine::check( Theory::Effort e ){
     }else if( e==Theory::EFFORT_FULL ){
       ++(d_statistics.d_instantiation_rounds);
     }
-
     Trace("quant-engine-debug") << "Check modules that needed check..." << std::endl;
     for( unsigned quant_e = QEFFORT_CONFLICT; quant_e<=QEFFORT_MODEL; quant_e++ ){
       bool success = true;
       //build the model if any module requested it
-      if( quant_e==QEFFORT_MODEL && needsModel ){
+      if( needsModelE==quant_e ){
         Assert( d_builder!=NULL );
         Trace("quant-engine-debug") << "Build model..." << std::endl;
         d_builder->d_addedLemmas = 0;
@@ -364,7 +365,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
       if( d_hasAddedLemma ){
         break;
       //otherwise, complete the model generation if necessary
-      }else if( quant_e==QEFFORT_MODEL && needsModel && options::produceModels() ){
+      }else if( quant_e==QEFFORT_MODEL && needsModelE<=quant_e && options::produceModels() ){
         Trace("quant-engine-debug") << "Build completed model..." << std::endl;
         d_builder->buildModel( d_model, true );
       }

diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 3ed6d369fc2d5ef224092d10963e4219120bc48a..1d8c1591c8e07c5a0d2a25dd4dde7e545d81f204 100644 (file)
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -55,9 +55,7 @@ public:
   /* whether this module needs to check this round */
   virtual bool needsCheck( Theory::Effort e ) { return e>=Theory::EFFORT_LAST_CALL; }
   /* whether this module needs a model built */
-  virtual bool needsModel( Theory::Effort e ) { return false; }
-  /* whether this module needs a model built */
-  virtual bool needsFullModel( Theory::Effort e ) { return false; }
+  virtual unsigned needsModel( Theory::Effort e );
   /* reset at a round */
   virtual void reset_round( Theory::Effort e ){}
   /* Call during quantifier engine's check */
@@ -143,6 +141,8 @@ public: //effort levels
     QEFFORT_CONFLICT,
     QEFFORT_STANDARD,
     QEFFORT_MODEL,
+    //none
+    QEFFORT_NONE,
   };
 private:
   /** list of all quantifiers seen */

diff --git a/test/regress/regress0/push-pop/bug326.smt2 b/test/regress/regress0/push-pop/bug326.smt2
index 8fe88e9f5f0ebc87e729a25c73b512f5d43bcdf2..f1506b3e81e247b3c91d8d8f04082755791cea7c 100644 (file)
--- a/test/regress/regress0/push-pop/bug326.smt2
+++ b/test/regress/regress0/push-pop/bug326.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --incremental
+; COMMAND-LINE: --incremental --rewrite-rules
 
 (set-logic AUFLIA)