Minor improvements to infrastructure. Minor changes to default options. Add tff script. Minor additions to sygus.

7 files changed, 23 insertions, 10 deletions

diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index e1fc9e793..5e6bcf0b4 100644
--- 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 f5077ad04..52e110720 100644
--- 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 6e73b37a7..1d6676464 100644
--- 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 8c53084f0..6cdb47be2 100644
--- 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 a529e37d0..4541c3d8a 100644
--- 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 e6f1ceee0..6c32ccb4a 100644
--- 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 db84ba885..37b1528b3 100644
--- 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{