Refactor modes for sygus+single invocation. Add option --inst-rlv-cond. Minor fixes...

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index cbef7109f57033bfea6bfc4ba8b58200915aaf8e..867feef6e51db776186ac66a12871fda00e2f330 100644 (file)
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -425,6 +425,24 @@ all \n\
 \n\
 ";
 
+const std::string OptionsHandler::s_cegqiSingleInvHelp = "\
+Modes for single invocation techniques, supported by --cegqi-si:\n\
+\n\
+none  \n\
++ Do not use single invocation techniques.\n\
+\n\
+use (default) \n\
++ Use single invocation techniques only if grammar is not restrictive.\n\
+\n\
+all-abort  \n\
++ Always use single invocation techniques, abort if solution reconstruction will likely fail,\
+  for instance, when the grammar does not have ITE and solution requires it.\n\
+\n\
+all \n\
++ Always use single invocation techniques. \n\
+\n\
+";
+
 const std::string OptionsHandler::s_sygusInvTemplHelp = "\
 Template modes for sygus invariant synthesis, supported by --sygus-inv-templ:\n\
 \n\
@@ -700,6 +718,24 @@ theory::quantifiers::IteLiftQuantMode OptionsHandler::stringToIteLiftQuantMode(s
   }
 }
 
+theory::quantifiers::CegqiSingleInvMode OptionsHandler::stringToCegqiSingleInvMode(std::string option, std::string optarg) throw(OptionException) {
+  if(optarg == "none" ) {
+    return theory::quantifiers::CEGQI_SI_MODE_NONE;
+  } else if(optarg == "use" || optarg == "default") {
+    return theory::quantifiers::CEGQI_SI_MODE_USE;
+  } else if(optarg == "all-abort") {
+    return theory::quantifiers::CEGQI_SI_MODE_ALL_ABORT;
+  } else if(optarg == "all") {
+    return theory::quantifiers::CEGQI_SI_MODE_ALL;
+  } else if(optarg ==  "help") {
+    puts(s_cegqiSingleInvHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --cegqi-si: `") +
+                          optarg + "'.  Try --cegqi-si help.");
+  }
+}
+
 theory::quantifiers::SygusInvTemplMode OptionsHandler::stringToSygusInvTemplMode(std::string option, std::string optarg) throw(OptionException) {
   if(optarg == "none" ) {
     return theory::quantifiers::SYGUS_INV_TEMPL_MODE_NONE;

diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index baa6cea9612374d50bf66ee655407594e0658eb1..8f23219ebb91844121cc820c4b780222a8b7d7ef 100644 (file)
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -98,6 +98,7 @@ public:
   theory::quantifiers::CegqiFairMode stringToCegqiFairMode(std::string option, std::string optarg) throw(OptionException);
   theory::quantifiers::TermDbMode stringToTermDbMode(std::string option, std::string optarg) throw(OptionException);
   theory::quantifiers::IteLiftQuantMode stringToIteLiftQuantMode(std::string option, std::string optarg) throw(OptionException);
+  theory::quantifiers::CegqiSingleInvMode stringToCegqiSingleInvMode(std::string option, std::string optarg) throw(OptionException);
   theory::quantifiers::SygusInvTemplMode stringToSygusInvTemplMode(std::string option, std::string optarg) throw(OptionException);
   theory::quantifiers::MacrosQuantMode stringToMacrosQuantMode(std::string option, std::string optarg) throw(OptionException);
   theory::quantifiers::QuantDSplitMode stringToQuantDSplitMode(std::string option, std::string optarg) throw(OptionException);
@@ -209,6 +210,7 @@ public:
   static const std::string s_qcfModeHelp;
   static const std::string s_qcfWhenModeHelp;
   static const std::string s_simplificationHelp;
+  static const std::string s_cegqiSingleInvHelp;
   static const std::string s_sygusInvTemplHelp;
   static const std::string s_termDbModeHelp;
   static const std::string s_theoryOfModeHelp;

diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h
index 38308c9dc0a028d56c57f49a13f60995fcd5f132..65445be17ebb777d49476e5d5c3e3de18aaff9a4 100644 (file)
--- a/src/options/quantifiers_modes.h
+++ b/src/options/quantifiers_modes.h
@@ -153,6 +153,17 @@ enum IteLiftQuantMode {
   ITE_LIFT_QUANT_MODE_ALL,
 };
 
+enum CegqiSingleInvMode {
+  /** do not use single invocation techniques */
+  CEGQI_SI_MODE_NONE,
+  /** use single invocation techniques */
+  CEGQI_SI_MODE_USE,
+  /** always use single invocation techniques, abort if solution reconstruction will fail */
+  CEGQI_SI_MODE_ALL_ABORT,
+  /** always use single invocation techniques */
+  CEGQI_SI_MODE_ALL,
+};
+
 enum SygusInvTemplMode {
   /** synthesize I( x ) */
   SYGUS_INV_TEMPL_MODE_NONE,

diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index 227540f454df23a13f88c29d1ac543a623e2daf9..456ab04c2c2eff23891f5cbe7e9e748995b2f6b7 100644 (file)
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -109,6 +109,9 @@ option instLevelInputOnly --inst-level-input-only bool :default true
  only input terms are assigned instantiation level zero
 option quantRepMode --quant-rep-mode=MODE  CVC4::theory::quantifiers::QuantRepMode :default CVC4::theory::quantifiers::QUANT_REP_MODE_FIRST :read-write :include "options/quantifiers_modes.h" :handler stringToQuantRepMode
  selection mode for representatives in quantifiers engine
+option instRelevantCond --inst-rlv-cond bool :default false
+ add relevancy conditions for instantiations
+
  
 option eagerInstQuant --eager-inst-quant bool :default false
  apply quantifier instantiation eagerly
@@ -229,8 +232,8 @@ option ceGuidedInst --cegqi bool :default false :read-write
   counterexample-guided quantifier instantiation
 option ceGuidedInstFair --cegqi-fair=MODE CVC4::theory::quantifiers::CegqiFairMode :default CVC4::theory::quantifiers::CEGQI_FAIR_DT_SIZE :include "options/quantifiers_modes.h" :handler stringToCegqiFairMode
   if and how to apply fairness for cegqi
-option cegqiSingleInv --cegqi-si bool :default false :read-write
-  process single invocation synthesis conjectures
+option cegqiSingleInvMode --cegqi-si=MODE CVC4::theory::quantifiers::CegqiSingleInvMode :default CVC4::theory::quantifiers::CEGQI_SI_MODE_NONE :include "options/quantifiers_modes.h" :handler stringToCegqiSingleInvMode :read-write
+  mode for processing single invocation synthesis conjectures
 option cegqiSingleInvPartial --cegqi-si-partial bool :default false
   combined techniques for synthesis conjectures that are partially single invocation 
 option cegqiSingleInvReconstruct --cegqi-si-reconstruct bool :default true
@@ -239,8 +242,6 @@ option cegqiSingleInvReconstructConst --cegqi-si-reconstruct-const bool :default
   include constants when reconstruct solutions for single invocation conjectures in original grammar
 option cegqiSingleInvAbort --cegqi-si-abort bool :default false
   abort if synthesis conjecture is not single invocation
-option cegqiSingleInvMultiInstAbort --cegqi-si-multi-inst-abort bool :default false
-  abort if synthesis conjecture is single invocation with no ITE in grammar and multiple instantiations are tried
   
 option sygusNormalForm --sygus-nf bool :default true
   only search for sygus builtin terms that are in normal form

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 54deba78c15703495a471e23f8629ed3f97a816f..62afbf987397d7217cd68ae1a4c1d2ba508a3d49 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1737,6 +1737,10 @@ void SmtEngine::setDefaults() {
       options::instMaxLevel.set( 0 );
     }
   }
+  if( options::instMaxLevel()!=-1 ){
+    Notice() << "SmtEngine: turning off cbqi to support instMaxLevel" << endl;
+    options::cbqi.set(false);
+  }
 
   if(options::fmfBoundIntLazy.wasSetByUser() && options::fmfBoundIntLazy()) {
     options::fmfBoundInt.set( true );
@@ -1797,13 +1801,15 @@ void SmtEngine::setDefaults() {
   }
 
   //apply counterexample guided instantiation options
-  if( options::cegqiSingleInv() ){
-    options::ceGuidedInst.set( true );
+  if( options::cegqiSingleInvMode()!=quantifiers::CEGQI_SI_MODE_NONE ){
+    if( !options::ceGuidedInst.wasSetByUser() ){
+      options::ceGuidedInst.set( true ); 
+    } 
   }
   if( options::ceGuidedInst() ){
     //counterexample-guided instantiation for sygus
-    if( !options::cegqiSingleInv.wasSetByUser() ){
-      options::cegqiSingleInv.set( true );
+    if( !options::cegqiSingleInvMode.wasSetByUser() ){
+      options::cegqiSingleInvMode.set( quantifiers::CEGQI_SI_MODE_USE );
     }
     if( !options::quantConflictFind.wasSetByUser() ){
       options::quantConflictFind.set( false );

diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index 8af11b1afaee339b7c2bf8709cec887a6b2368f4..71bf7c4266125a14ab460690f7506d7a58d8eb64 100644 (file)
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -48,7 +48,7 @@ void CegConjecture::assign( Node q ) {
   Assert( q.getKind()==FORALL );
   d_assert_quant = q;
   //register with single invocation if applicable
-  if( d_qe->getTermDatabase()->isQAttrSygus( d_assert_quant ) && options::cegqiSingleInv() ){
+  if( d_qe->getTermDatabase()->isQAttrSygus( d_assert_quant ) && options::cegqiSingleInvMode()!=CEGQI_SI_MODE_NONE ){
     d_ceg_si->initialize( q );
     if( q!=d_ceg_si->d_quant ){
       //Node red_lem = NodeManager::currentNM()->mkNode( OR, q.negate(), d_cegqi_si->d_quant );

diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index a5d4174dd6c277062cbb1fec06225370e66a13da..3177739ac7092452e0cfdcf49a501acf2e309b22 100644 (file)
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -111,6 +111,7 @@ void CegConjectureSingleInv::getInitialSingleInvLemma( std::vector< Node >& lems
 
 void CegConjectureSingleInv::initialize( Node q ) {
   Assert( d_quant.isNull() );
+  Assert( options::cegqiSingleInvMode()!=CEGQI_SI_MODE_NONE );
   //initialize data
   d_quant = q;
   //process
@@ -121,6 +122,7 @@ void CegConjectureSingleInv::initialize( Node q ) {
   std::map< Node, std::map< Node, std::vector< Node > > > prog_invoke;
   std::vector< Node > progs;
   std::map< Node, std::map< Node, bool > > contains;
+  bool is_syntax_restricted = false;
   for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
     progs.push_back( q[0][i] );
     //check whether all types have ITE
@@ -131,161 +133,173 @@ void CegConjectureSingleInv::initialize( Node q ) {
         d_has_ites = false;
       }
     }
+    Assert( datatypes::DatatypesRewriter::isTypeDatatype(tn) );
+    const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+    Assert( dt.isSygus() );
+    if( !dt.getSygusAllowAll() ){
+      is_syntax_restricted = true;
+    }
   }
-  Node qq = q[1];
-  if( q[1].getKind()==NOT && q[1][0].getKind()==FORALL ){
-    qq = q[1][0][1];
-  }else{
-    qq = TermDb::simpleNegate( qq );
-  }
-  //remove the deep embedding
-  std::map< Node, Node > visited;
-  std::vector< TypeNode > types;
-  std::vector< Node > order_vars;
-  std::map< Node, Node > single_inv_app_map;
-  int type_valid = 0;
-  qq = removeDeepEmbedding( qq, progs, types, type_valid, visited );
-  Trace("cegqi-si-debug") << "- Remove deep embedding, got : " << qq << ", type valid = " << type_valid << std::endl;
+  //abort if not aggressive
   bool singleInvocation = true;
-  if( type_valid==0 ){
-    //process the single invocation-ness of the property
-    d_sip->init( types, qq );
-    Trace("cegqi-si") << "- Partitioned to single invocation parts : " << std::endl;
-    d_sip->debugPrint( "cegqi-si" );
-    //map from program to bound variables
-    for( unsigned j=0; j<progs.size(); j++ ){
-      Node prog = progs[j];
-      std::map< Node, Node >::iterator it_nsi = d_nsi_op_map.find( prog );
-      if( it_nsi!=d_nsi_op_map.end() ){
-        Node op = it_nsi->second;
-        std::map< Node, Node >::iterator it_fov = d_sip->d_func_fo_var.find( op );
-        if( it_fov!=d_sip->d_func_fo_var.end() ){
-          Node pv = it_fov->second;
-          Assert( d_sip->d_func_inv.find( op )!=d_sip->d_func_inv.end() );
-          Node inv = d_sip->d_func_inv[op];
-          single_inv_app_map[prog] = inv;
-          Trace("cegqi-si") << "  " << pv << ", " << inv << " is associated with program " << prog << std::endl;
-          d_prog_to_sol_index[prog] = order_vars.size();
-          order_vars.push_back( pv );
+  if( options::cegqiSingleInvMode()==CEGQI_SI_MODE_USE && is_syntax_restricted ){
+    singleInvocation = false;
+    Trace("cegqi-si") << "...grammar is restricted, do not use single invocation techniques." << std::endl;
+  }else{  
+    Node qq = q[1];
+    if( q[1].getKind()==NOT && q[1][0].getKind()==FORALL ){
+      qq = q[1][0][1];
+    }else{
+      qq = TermDb::simpleNegate( qq );
+    }
+    //remove the deep embedding
+    std::map< Node, Node > visited;
+    std::vector< TypeNode > types;
+    std::vector< Node > order_vars;
+    std::map< Node, Node > single_inv_app_map;
+    int type_valid = 0;
+    qq = removeDeepEmbedding( qq, progs, types, type_valid, visited );
+    Trace("cegqi-si-debug") << "- Remove deep embedding, got : " << qq << ", type valid = " << type_valid << std::endl;
+    if( type_valid==0 ){
+      //process the single invocation-ness of the property
+      d_sip->init( types, qq );
+      Trace("cegqi-si") << "- Partitioned to single invocation parts : " << std::endl;
+      d_sip->debugPrint( "cegqi-si" );
+      //map from program to bound variables
+      for( unsigned j=0; j<progs.size(); j++ ){
+        Node prog = progs[j];
+        std::map< Node, Node >::iterator it_nsi = d_nsi_op_map.find( prog );
+        if( it_nsi!=d_nsi_op_map.end() ){
+          Node op = it_nsi->second;
+          std::map< Node, Node >::iterator it_fov = d_sip->d_func_fo_var.find( op );
+          if( it_fov!=d_sip->d_func_fo_var.end() ){
+            Node pv = it_fov->second;
+            Assert( d_sip->d_func_inv.find( op )!=d_sip->d_func_inv.end() );
+            Node inv = d_sip->d_func_inv[op];
+            single_inv_app_map[prog] = inv;
+            Trace("cegqi-si") << "  " << pv << ", " << inv << " is associated with program " << prog << std::endl;
+            d_prog_to_sol_index[prog] = order_vars.size();
+            order_vars.push_back( pv );
+          }
+        }else{
+          //does not mention the function
         }
-      }else{
-        //does not mention the function
       }
-    }
-    //reorder the variables
-    Assert( d_sip->d_func_vars.size()==order_vars.size() );
-    d_sip->d_func_vars.clear();
-    d_sip->d_func_vars.insert( d_sip->d_func_vars.begin(), order_vars.begin(), order_vars.end() );
+      //reorder the variables
+      Assert( d_sip->d_func_vars.size()==order_vars.size() );
+      d_sip->d_func_vars.clear();
+      d_sip->d_func_vars.insert( d_sip->d_func_vars.begin(), order_vars.begin(), order_vars.end() );
 
-    //check if it is single invocation
-    if( !d_sip->d_conjuncts[1].empty() ){
-      singleInvocation = false;
-      if( options::cegqiSingleInvPartial() ){
-        //this enables partially single invocation techniques
-        d_nsingle_inv = d_sip->getNonSingleInvocation();
-        d_nsingle_inv = TermDb::simpleNegate( d_nsingle_inv );
-        d_full_inv = d_sip->getFullSpecification();
-        d_full_inv = TermDb::simpleNegate( d_full_inv );
-        singleInvocation = true;
-      }else if( options::sygusInvTemplMode() != SYGUS_INV_TEMPL_MODE_NONE ){
-        //if we are doing invariant templates, then construct the template
-        std::map< Node, bool > has_inv;
-        std::map< Node, std::vector< Node > > inv_pre_post[2];
-        for( unsigned i=0; i<d_sip->d_conjuncts[2].size(); i++ ){
-          std::vector< Node > disjuncts;
-          Node func;
-          int pol = -1;
-          Trace("cegqi-inv") << "INV process " << d_sip->d_conjuncts[2][i] << std::endl;
-          d_sip->extractInvariant( d_sip->d_conjuncts[2][i], func, pol, disjuncts );
-          if( pol>=0 ){
-            Assert( d_nsi_op_map_to_prog.find( func )!=d_nsi_op_map_to_prog.end() );
-            Node prog = d_nsi_op_map_to_prog[func];
-            Trace("cegqi-inv") << "..." << ( pol==0 ? "pre" : "post" ) << "-condition for " << prog << "." << std::endl;
-            Node c = disjuncts.empty() ? d_qe->getTermDatabase()->d_false : ( disjuncts.size()==1 ? disjuncts[0] : NodeManager::currentNM()->mkNode( OR, disjuncts ) );
-            c = pol==0 ? TermDb::simpleNegate( c ) : c;
-            Trace("cegqi-inv-debug") << "...extracted : " << c << std::endl;
-            inv_pre_post[pol][prog].push_back( c );
-            has_inv[prog] = true;
-          }else{
-            Trace("cegqi-inv") << "...no status." << std::endl;
+      //check if it is single invocation
+      if( !d_sip->d_conjuncts[1].empty() ){
+        singleInvocation = false;
+        if( options::cegqiSingleInvPartial() ){
+          //this enables partially single invocation techniques
+          d_nsingle_inv = d_sip->getNonSingleInvocation();
+          d_nsingle_inv = TermDb::simpleNegate( d_nsingle_inv );
+          d_full_inv = d_sip->getFullSpecification();
+          d_full_inv = TermDb::simpleNegate( d_full_inv );
+          singleInvocation = true;
+        }else if( options::sygusInvTemplMode() != SYGUS_INV_TEMPL_MODE_NONE ){
+          //if we are doing invariant templates, then construct the template
+          std::map< Node, bool > has_inv;
+          std::map< Node, std::vector< Node > > inv_pre_post[2];
+          for( unsigned i=0; i<d_sip->d_conjuncts[2].size(); i++ ){
+            std::vector< Node > disjuncts;
+            Node func;
+            int pol = -1;
+            Trace("cegqi-inv") << "INV process " << d_sip->d_conjuncts[2][i] << std::endl;
+            d_sip->extractInvariant( d_sip->d_conjuncts[2][i], func, pol, disjuncts );
+            if( pol>=0 ){
+              Assert( d_nsi_op_map_to_prog.find( func )!=d_nsi_op_map_to_prog.end() );
+              Node prog = d_nsi_op_map_to_prog[func];
+              Trace("cegqi-inv") << "..." << ( pol==0 ? "pre" : "post" ) << "-condition for " << prog << "." << std::endl;
+              Node c = disjuncts.empty() ? d_qe->getTermDatabase()->d_false : ( disjuncts.size()==1 ? disjuncts[0] : NodeManager::currentNM()->mkNode( OR, disjuncts ) );
+              c = pol==0 ? TermDb::simpleNegate( c ) : c;
+              Trace("cegqi-inv-debug") << "...extracted : " << c << std::endl;
+              inv_pre_post[pol][prog].push_back( c );
+              has_inv[prog] = true;
+            }else{
+              Trace("cegqi-inv") << "...no status." << std::endl;
+            }
           }
-        }
 
-        Trace("cegqi-inv") << "Constructing invariant templates..." << std::endl;
-        //now, contruct the template for the invariant(s)
-        std::map< Node, Node > prog_templ;
-        for( std::map< Node, bool >::iterator iti = has_inv.begin(); iti != has_inv.end(); ++iti ){
-          Node prog = iti->first;
-          Trace("cegqi-inv") << "...for " << prog << "..." << std::endl;
-          Trace("cegqi-inv") << "   args : ";
+          Trace("cegqi-inv") << "Constructing invariant templates..." << std::endl;
+          //now, contruct the template for the invariant(s)
+          std::map< Node, Node > prog_templ;
+          for( std::map< Node, bool >::iterator iti = has_inv.begin(); iti != has_inv.end(); ++iti ){
+            Node prog = iti->first;
+            Trace("cegqi-inv") << "...for " << prog << "..." << std::endl;
+            Trace("cegqi-inv") << "   args : ";
+            for( unsigned j=0; j<d_sip->d_si_vars.size(); j++ ){
+              std::stringstream ss;
+              ss << "i_" << j;
+              Node v = NodeManager::currentNM()->mkBoundVar( ss.str(), d_sip->d_si_vars[j].getType() );
+              d_prog_templ_vars[prog].push_back( v );
+              Trace("cegqi-inv") << v << " ";
+            }
+            Trace("cegqi-inv") << std::endl;
+            Node pre = inv_pre_post[0][prog].empty() ? NodeManager::currentNM()->mkConst( false ) :
+                        ( inv_pre_post[0][prog].size()==1 ? inv_pre_post[0][prog][0] : NodeManager::currentNM()->mkNode( OR, inv_pre_post[0][prog] ) );
+            d_trans_pre[prog] = pre.substitute( d_sip->d_si_vars.begin(), d_sip->d_si_vars.end(), d_prog_templ_vars[prog].begin(), d_prog_templ_vars[prog].end() );
+            Node post = inv_pre_post[1][prog].empty() ? NodeManager::currentNM()->mkConst( true ) :
+                        ( inv_pre_post[1][prog].size()==1 ? inv_pre_post[1][prog][0] : NodeManager::currentNM()->mkNode( AND, inv_pre_post[1][prog] ) );
+            d_trans_post[prog] = post.substitute( d_sip->d_si_vars.begin(), d_sip->d_si_vars.end(), d_prog_templ_vars[prog].begin(), d_prog_templ_vars[prog].end() );
+            Trace("cegqi-inv") << "   precondition : " << d_trans_pre[prog] << std::endl;
+            Trace("cegqi-inv") << "  postcondition : " << d_trans_post[prog] << std::endl;
+            Node invariant = single_inv_app_map[prog];
+            invariant = invariant.substitute( d_sip->d_si_vars.begin(), d_sip->d_si_vars.end(), d_prog_templ_vars[prog].begin(), d_prog_templ_vars[prog].end() );
+            Trace("cegqi-inv") << "      invariant : " << invariant << std::endl;
+            //construct template
+            Node templ;
+            if( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_PRE ){
+              //templ = NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( OR, d_trans_pre[prog], invariant ), d_trans_post[prog] );
+              templ = NodeManager::currentNM()->mkNode( OR, d_trans_pre[prog], invariant );
+            }else{
+              Assert( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_POST );
+              //templ = NodeManager::currentNM()->mkNode( OR, d_trans_pre[prog], NodeManager::currentNM()->mkNode( AND, d_trans_post[prog], invariant ) );
+              templ = NodeManager::currentNM()->mkNode( AND, d_trans_post[prog], invariant );
+            }
+            visited.clear();
+            templ = addDeepEmbedding( templ, visited );
+            Trace("cegqi-inv") << "       template : " << templ << std::endl;
+            prog_templ[prog] = templ;
+          }
+          Node bd = d_sip->d_conjuncts[2].size()==1 ? d_sip->d_conjuncts[2][0] : NodeManager::currentNM()->mkNode( AND, d_sip->d_conjuncts[2] );
+          visited.clear();
+          bd = addDeepEmbedding( bd, visited );
+          Trace("cegqi-inv") << "           body : " << bd << std::endl;
+          bd = substituteInvariantTemplates( bd, prog_templ, d_prog_templ_vars );
+          Trace("cegqi-inv-debug") << "     templ-subs body : " << bd << std::endl;
+          //make inner existential
+          std::vector< Node > new_var_bv;
           for( unsigned j=0; j<d_sip->d_si_vars.size(); j++ ){
             std::stringstream ss;
-            ss << "i_" << j;
-            Node v = NodeManager::currentNM()->mkBoundVar( ss.str(), d_sip->d_si_vars[j].getType() );
-            d_prog_templ_vars[prog].push_back( v );
-            Trace("cegqi-inv") << v << " ";
+            ss << "ss_" << j;
+            new_var_bv.push_back( NodeManager::currentNM()->mkBoundVar( ss.str(), d_sip->d_si_vars[j].getType() ) );
           }
-          Trace("cegqi-inv") << std::endl;
-          Node pre = inv_pre_post[0][prog].empty() ? NodeManager::currentNM()->mkConst( false ) :
-                      ( inv_pre_post[0][prog].size()==1 ? inv_pre_post[0][prog][0] : NodeManager::currentNM()->mkNode( OR, inv_pre_post[0][prog] ) );
-          d_trans_pre[prog] = pre.substitute( d_sip->d_si_vars.begin(), d_sip->d_si_vars.end(), d_prog_templ_vars[prog].begin(), d_prog_templ_vars[prog].end() );
-          Node post = inv_pre_post[1][prog].empty() ? NodeManager::currentNM()->mkConst( true ) :
-                      ( inv_pre_post[1][prog].size()==1 ? inv_pre_post[1][prog][0] : NodeManager::currentNM()->mkNode( AND, inv_pre_post[1][prog] ) );
-          d_trans_post[prog] = post.substitute( d_sip->d_si_vars.begin(), d_sip->d_si_vars.end(), d_prog_templ_vars[prog].begin(), d_prog_templ_vars[prog].end() );
-          Trace("cegqi-inv") << "   precondition : " << d_trans_pre[prog] << std::endl;
-          Trace("cegqi-inv") << "  postcondition : " << d_trans_post[prog] << std::endl;
-          Node invariant = single_inv_app_map[prog];
-          invariant = invariant.substitute( d_sip->d_si_vars.begin(), d_sip->d_si_vars.end(), d_prog_templ_vars[prog].begin(), d_prog_templ_vars[prog].end() );
-          Trace("cegqi-inv") << "      invariant : " << invariant << std::endl;
-          //construct template
-          Node templ;
-          if( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_PRE ){
-            //templ = NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( OR, d_trans_pre[prog], invariant ), d_trans_post[prog] );
-            templ = NodeManager::currentNM()->mkNode( OR, d_trans_pre[prog], invariant );
-          }else{
-            Assert( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_POST );
-            //templ = NodeManager::currentNM()->mkNode( OR, d_trans_pre[prog], NodeManager::currentNM()->mkNode( AND, d_trans_post[prog], invariant ) );
-            templ = NodeManager::currentNM()->mkNode( AND, d_trans_post[prog], invariant );
+          bd = bd.substitute( d_sip->d_si_vars.begin(), d_sip->d_si_vars.end(), new_var_bv.begin(), new_var_bv.end() );
+          Assert( q[1].getKind()==NOT && q[1][0].getKind()==FORALL );
+          for( unsigned j=0; j<q[1][0][0].getNumChildren(); j++ ){
+            new_var_bv.push_back( q[1][0][0][j] );
           }
-          visited.clear();
-          templ = addDeepEmbedding( templ, visited );
-          Trace("cegqi-inv") << "       template : " << templ << std::endl;
-          prog_templ[prog] = templ;
-        }
-        Node bd = d_sip->d_conjuncts[2].size()==1 ? d_sip->d_conjuncts[2][0] : NodeManager::currentNM()->mkNode( AND, d_sip->d_conjuncts[2] );
-        visited.clear();
-        bd = addDeepEmbedding( bd, visited );
-        Trace("cegqi-inv") << "           body : " << bd << std::endl;
-        bd = substituteInvariantTemplates( bd, prog_templ, d_prog_templ_vars );
-        Trace("cegqi-inv-debug") << "     templ-subs body : " << bd << std::endl;
-        //make inner existential
-        std::vector< Node > new_var_bv;
-        for( unsigned j=0; j<d_sip->d_si_vars.size(); j++ ){
-          std::stringstream ss;
-          ss << "ss_" << j;
-          new_var_bv.push_back( NodeManager::currentNM()->mkBoundVar( ss.str(), d_sip->d_si_vars[j].getType() ) );
-        }
-        bd = bd.substitute( d_sip->d_si_vars.begin(), d_sip->d_si_vars.end(), new_var_bv.begin(), new_var_bv.end() );
-        Assert( q[1].getKind()==NOT && q[1][0].getKind()==FORALL );
-        for( unsigned j=0; j<q[1][0][0].getNumChildren(); j++ ){
-          new_var_bv.push_back( q[1][0][0][j] );
-        }
-        if( !new_var_bv.empty() ){
-          Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, new_var_bv );
-          bd = NodeManager::currentNM()->mkNode( FORALL, bvl, bd ).negate();
+          if( !new_var_bv.empty() ){
+            Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, new_var_bv );
+            bd = NodeManager::currentNM()->mkNode( FORALL, bvl, bd ).negate();
+          }
+          //make outer universal
+          bd = NodeManager::currentNM()->mkNode( FORALL, q[0], bd );
+          bd = Rewriter::rewrite( bd );
+          Trace("cegqi-inv") << "  rtempl-subs body : " << bd << std::endl;
+          d_quant = bd;
         }
-        //make outer universal
-        bd = NodeManager::currentNM()->mkNode( FORALL, q[0], bd );
-        bd = Rewriter::rewrite( bd );
-        Trace("cegqi-inv") << "  rtempl-subs body : " << bd << std::endl;
-        d_quant = bd;
+      }else{
+        //we are fully single invocation
       }
     }else{
-      //we are fully single invocation
+      Trace("cegqi-si") << "...property is not single invocation, involves functions with different argument sorts." << std::endl;
+      singleInvocation = false;
     }
-  }else{
-    Trace("cegqi-si") << "...property is not single invocation, involves functions with different argument sorts." << std::endl;
-    singleInvocation = false;
   }
   if( singleInvocation ){
     d_single_inv = d_sip->getSingleInvocation();
@@ -829,8 +843,8 @@ Node CegConjectureSingleInv::reconstructToSyntax( Node s, TypeNode stn, int& rec
 }
 
 bool CegConjectureSingleInv::needsCheck() {
-  if( options::cegqiSingleInvMultiInstAbort() ){
-    if( !hasITEs() ){
+  if( options::cegqiSingleInvMode()==CEGQI_SI_MODE_ALL_ABORT ){
+    if( !d_has_ites ){
       return d_inst.empty();
     }
   }

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index e8124503458399defc7da44fdbac48c591e3d962..334e42375067021f1f2cd6c2629477da0887fafb 100644 (file)
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1865,6 +1865,18 @@ bool TermDb::getEnsureTypeCondition( Node n, TypeNode tn, std::vector< Node >& c
   }
 }
 
+void TermDb::getRelevancyCondition( Node n, std::vector< Node >& cond ) {
+  if( n.getKind()==APPLY_SELECTOR_TOTAL ){
+    unsigned scindex = Datatype::cindexOf(n.getOperator().toExpr());
+    const Datatype& dt = ((DatatypeType)(n[0].getType()).toType()).getDatatype();
+    Node rc = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[scindex].getTester() ), n[0] ).negate();
+    if( std::find( cond.begin(), cond.end(), rc )==cond.end() ){
+      cond.push_back( rc );
+    }
+    getRelevancyCondition( n[0], cond );
+  }
+}
+
 bool TermDb::containsTerm2( Node n, Node t, std::map< Node, bool >& visited ) {
   if( n==t ){
     return true;

diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index b7b798cd49845b45857b1fcaf5cf345ea852fdfe..3f931014b6b0c06b4e0a7129481316fc0b32d1c3 100644 (file)
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -462,6 +462,8 @@ public:
   static Node ensureType( Node n, TypeNode tn );
   /** get ensure type condition */
   static bool getEnsureTypeCondition( Node n, TypeNode tn, std::vector< Node >& cond );
+  /** get relevancy condition */
+  static void getRelevancyCondition( Node n, std::vector< Node >& cond );
 private:
   //helper for contains term
   static bool containsTerm2( Node n, Node t, std::map< Node, bool >& visited );

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 8984cc5f4fe22d15bd7c09531d179739521ef01b..ebf89c0b8c646b5a9d615b545d9b14db39f2dedd 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -1010,6 +1010,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo
   Assert( !d_conflict );
   Assert( terms.size()==q[0].getNumChildren() );
   Trace("inst-add-debug") << "For quantified formula " << q << ", add instantiation: " << std::endl;
+  std::vector< Node > rlv_cond;
   for( unsigned i=0; i<terms.size(); i++ ){
     Trace("inst-add-debug") << "  " << q[0][i];
     Trace("inst-add-debug2") << " -> " << terms[i];
@@ -1027,6 +1028,11 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo
     if( terms[i].isNull() ){
       Trace("inst-add-debug") << " --> Failed to make term vector, due to term/type restrictions." << std::endl;
       return false;
+    }else{
+      //get relevancy conditions
+      if( options::instRelevantCond() ){
+        quantifiers::TermDb::getRelevancyCondition( terms[i], rlv_cond );
+      }
     }
 #ifdef CVC4_ASSERTIONS
     bool bad_inst = false;
@@ -1092,14 +1098,21 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo
   Trace("inst-add-debug") << "Constructing instantiation..." << std::endl;
   Assert( d_term_db->d_vars[q].size()==terms.size() );
   Node body = getInstantiation( q, d_term_db->d_vars[q], terms, doVts );  //do virtual term substitution
+  Node orig_body = body;
   body = quantifiers::QuantifiersRewriter::preprocess( body, true );
   Trace("inst-debug") << "...preprocess to " << body << std::endl;
 
   //construct the lemma
   Trace("inst-assert") << "(assert " << body << ")" << std::endl;
-  Node orig_body = body;
   body = Rewriter::rewrite(body);
-  Node lem = NodeManager::currentNM()->mkNode( kind::OR, q.negate(), body );
+  Node lem;
+  if( rlv_cond.empty() ){
+    lem = NodeManager::currentNM()->mkNode( kind::OR, q.negate(), body );
+  }else{
+    rlv_cond.push_back( q.negate() );
+    rlv_cond.push_back( body );
+    lem = NodeManager::currentNM()->mkNode( kind::OR, rlv_cond );
+  }
   lem = Rewriter::rewrite(lem);
 
   //check for lemma duplication
@@ -1120,15 +1133,20 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo
       }
     }
     if( options::instMaxLevel()!=-1 ){
-      uint64_t maxInstLevel = 0;
-      for( unsigned i=0; i<terms.size(); i++ ){
-        if( terms[i].hasAttribute(InstLevelAttribute()) ){
-          if( terms[i].getAttribute(InstLevelAttribute())>maxInstLevel ){
-            maxInstLevel = terms[i].getAttribute(InstLevelAttribute());
+      if( doVts ){
+        //virtual term substitution/instantiation level features are incompatible
+        Assert( false );
+      }else{
+        uint64_t maxInstLevel = 0;
+        for( unsigned i=0; i<terms.size(); i++ ){
+          if( terms[i].hasAttribute(InstLevelAttribute()) ){
+            if( terms[i].getAttribute(InstLevelAttribute())>maxInstLevel ){
+              maxInstLevel = terms[i].getAttribute(InstLevelAttribute());
+            }
           }
         }
+        setInstantiationLevelAttr( orig_body, q[1], maxInstLevel+1 );
       }
-      setInstantiationLevelAttr( orig_body, q[1], maxInstLevel+1 );
     }
     if( d_curr_effort_level>QEFFORT_CONFLICT && d_curr_effort_level<QEFFORT_NONE ){
       //notify listeners

diff --git a/test/regress/regress0/sygus/array_search_2.sy b/test/regress/regress0/sygus/array_search_2.sy
index 56a30b2109609abc37eecde165648b763ecaf9c8..e6683ced98c0300afc414056789d186192693274 100644 (file)
--- a/test/regress/regress0/sygus/array_search_2.sy
+++ b/test/regress/regress0/sygus/array_search_2.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --no-dump-synth
 (set-logic LIA)
 (synth-fun findIdx ( (y1 Int) (y2 Int) (k1 Int)) Int ((Start Int ( 0 1 2 y1 y2 k1 (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start)))))
 (declare-var x1 Int)

diff --git a/test/regress/regress0/sygus/array_sum_2_5.sy b/test/regress/regress0/sygus/array_sum_2_5.sy
index f6c0320e20ef5a09e21a1695c8979336b99716d8..387ce94870ff3920fcb9946fe794d35dc6786358 100644 (file)
--- a/test/regress/regress0/sygus/array_sum_2_5.sy
+++ b/test/regress/regress0/sygus/array_sum_2_5.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --no-dump-synth
 (set-logic LIA)
 (synth-fun findSum ( (y1 Int) (y2 Int) )Int ((Start Int ( 0 1 2 y1 y2 (+ Start Start)    (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start)))))
 (declare-var x1 Int)

diff --git a/test/regress/regress0/sygus/clock-inc-tuple.sy b/test/regress/regress0/sygus/clock-inc-tuple.sy
index 09bdb8b4d028e0f5a6b38d18ced74e2ccd807d34..3519319bd11a25fd5f1c49b7032b148ed9eb5693 100644 (file)
--- a/test/regress/regress0/sygus/clock-inc-tuple.sy
+++ b/test/regress/regress0/sygus/clock-inc-tuple.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --no-dump-synth
 
 (set-logic ALL_SUPPORTED)
 (declare-var m Int)

diff --git a/test/regress/regress0/sygus/commutative.sy b/test/regress/regress0/sygus/commutative.sy
index 46dbd29815f70d48fd59a852f00db7c56b334a43..f675bddad7cae1c87d0e072c4d070922b12a77e3 100644 (file)
--- a/test/regress/regress0/sygus/commutative.sy
+++ b/test/regress/regress0/sygus/commutative.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi --no-dump-synth
+; COMMAND-LINE: --no-dump-synth
 
 (set-logic LIA)
 
@@ -19,4 +19,4 @@
 
 (check-synth)
 
-; (+ x y) is a valid solution
\ No newline at end of file
+; (+ x y) is a valid solution

diff --git a/test/regress/regress0/sygus/const-var-test.sy b/test/regress/regress0/sygus/const-var-test.sy
index 428cb2adc61b008efd31faad319a2346931e7aaa..b79b7eeec6b4118a0af2a30c194675b252d2d6ef 100644 (file)
--- a/test/regress/regress0/sygus/const-var-test.sy
+++ b/test/regress/regress0/sygus/const-var-test.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --no-dump-synth
 
 (set-logic LIA)
 

diff --git a/test/regress/regress0/sygus/constant.sy b/test/regress/regress0/sygus/constant.sy
index 0059f6947c74cc5e857d752d254165e8a77ccc66..5c48f5e39cc80a9f1ce8d4ee2c9f988bce78105b 100644 (file)
--- a/test/regress/regress0/sygus/constant.sy
+++ b/test/regress/regress0/sygus/constant.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi --no-dump-synth
+; COMMAND-LINE: --no-dump-synth
 
 (set-logic LIA)
 
@@ -20,4 +20,4 @@
 
 (check-synth)
 
-; 0, 1, (- x x) are valid solutions
\ No newline at end of file
+; 0, 1, (- x x) are valid solutions

diff --git a/test/regress/regress0/sygus/dt-no-syntax.sy b/test/regress/regress0/sygus/dt-no-syntax.sy
index e0f8112ce2406da3e46943d646b86f5cfe934d99..42382ac91fd13c2a74d074c932704309039010f3 100644 (file)
--- a/test/regress/regress0/sygus/dt-no-syntax.sy
+++ b/test/regress/regress0/sygus/dt-no-syntax.sy
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cegqi --no-dump-synth
+; COMMAND-LINE: --no-dump-synth
 ; EXPECT: unsat
 (set-logic LIA)
 

diff --git a/test/regress/regress0/sygus/dt-test-ns.sy b/test/regress/regress0/sygus/dt-test-ns.sy
index ed17f4ff2b4b7e67e1eb926483805e8d3a95d4d1..0520650614a2f22b05bb55c8dec0792d2451dc41 100644 (file)
--- a/test/regress/regress0/sygus/dt-test-ns.sy
+++ b/test/regress/regress0/sygus/dt-test-ns.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --no-dump-synth
 (set-logic LIA)
 
 (declare-datatypes () ((List (cons (head Int) (tail List)) (nil))))

diff --git a/test/regress/regress0/sygus/dup-op.sy b/test/regress/regress0/sygus/dup-op.sy
index e5448d6268cae88255b51324920ac2aebedba9ca..bed9972fdba7a6499dab6c26b216e7cb7a56de85 100644 (file)
--- a/test/regress/regress0/sygus/dup-op.sy
+++ b/test/regress/regress0/sygus/dup-op.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi --no-cegqi-si --no-dump-synth
+; COMMAND-LINE: --cegqi-si=none --no-dump-synth
 (set-logic LIA)
 (synth-fun f ((x Int)) Int
     ((Start Int ((+ Con Con) (+ Start Start) x))

diff --git a/test/regress/regress0/sygus/enum-test.sy b/test/regress/regress0/sygus/enum-test.sy
index cd129385e353672661d46838955edca0b5d683d3..7b59f5f1a6ee0489740e1599b92d362dd2eeb12d 100644 (file)
--- a/test/regress/regress0/sygus/enum-test.sy
+++ b/test/regress/regress0/sygus/enum-test.sy
@@ -1,8 +1,8 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --no-dump-synth
 (set-logic LIA)
 (define-sort D (Enum (a b)))
 (define-fun f ((x D)) Int (ite (= x D::a) 3 7))
 (synth-fun g () D ((Start D (D::a D::b))))
 (constraint (= (f g) 7))
-(check-synth)
\ No newline at end of file
+(check-synth)

diff --git a/test/regress/regress0/sygus/hd-sdiv.sy b/test/regress/regress0/sygus/hd-sdiv.sy
index 3ac9334b21d645e59815a9841037048b670d27a9..019b48a1c1624ed1a848c4a01f3fb0fb48ec2c6b 100644 (file)
--- a/test/regress/regress0/sygus/hd-sdiv.sy
+++ b/test/regress/regress0/sygus/hd-sdiv.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi --no-cegqi-si --no-dump-synth
+; COMMAND-LINE: --cegqi-si=none --no-dump-synth
 (set-logic BV)
 
 (define-fun hd01 ((x (BitVec 32))) (BitVec 32) (bvand x #x00000001))

diff --git a/test/regress/regress0/sygus/icfp_28_10.sy b/test/regress/regress0/sygus/icfp_28_10.sy
index b07be0e98f9ab8ae9738fccbf7a4de2751ec075f..74e054159e229aad9bb6660a300becab0fab6144 100644 (file)
--- a/test/regress/regress0/sygus/icfp_28_10.sy
+++ b/test/regress/regress0/sygus/icfp_28_10.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi --no-dump-synth
+; COMMAND-LINE: --no-dump-synth
 
 (set-logic BV)
 

diff --git a/test/regress/regress0/sygus/inv-example.sy b/test/regress/regress0/sygus/inv-example.sy
index aafbbd9879cf8683675a04ab45fd08e6ae8aae86..b5642596417d532c1761cd13329942ce639fe7c7 100644 (file)
--- a/test/regress/regress0/sygus/inv-example.sy
+++ b/test/regress/regress0/sygus/inv-example.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si --no-dump-synth
+; COMMAND-LINE: --no-dump-synth
 (set-logic LIA)
 (synth-inv inv-f ((x Int) (y Int) (b Bool)))
 (declare-primed-var x Int)
@@ -9,4 +9,4 @@
 (define-fun trans-f ((x Int) (y Int) (b Bool) (x! Int) (y! Int) (b! Bool)) Bool (and (and (= b! b) (= y! x)) (ite b (= x! (+ x 10)) (= x! (+ x 12)))))
 (define-fun post-f ((x Int) (y Int) (b Bool)) Bool (<= y x))
 (inv-constraint inv-f pre-f trans-f post-f)
-(check-synth)
\ No newline at end of file
+(check-synth)

diff --git a/test/regress/regress0/sygus/let-ringer.sy b/test/regress/regress0/sygus/let-ringer.sy
index 4bae90b001293524c1836a802c3c99142bfcf09e..d5d40ace4d30d4dd7c4b2e596eafe2a942f7bc89 100644 (file)
--- a/test/regress/regress0/sygus/let-ringer.sy
+++ b/test/regress/regress0/sygus/let-ringer.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --no-dump-synth
 (set-logic LIA)
 (define-fun g ((x Int)) Int (ite (= x 1) 15 19))
 (synth-fun f ((x Int)) Int

diff --git a/test/regress/regress0/sygus/let-simp.sy b/test/regress/regress0/sygus/let-simp.sy
index 71cd27e8f1070fbe9da7574cf43dea27e3eea5b9..d07f6a717d9c67127824a09b0f4a8f910bcddf3b 100644 (file)
--- a/test/regress/regress0/sygus/let-simp.sy
+++ b/test/regress/regress0/sygus/let-simp.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --no-dump-synth
 (set-logic LIA)
 (synth-fun f ((x Int) (y Int)) Int
     ((Start Int (x

diff --git a/test/regress/regress0/sygus/list-head-x.sy b/test/regress/regress0/sygus/list-head-x.sy
index a5977d1e7c3891a26a2436c59a4f4f7d3f592a15..21362dc2cfd4ee25f569c7d2ae2df53b5098a0a0 100644 (file)
--- a/test/regress/regress0/sygus/list-head-x.sy
+++ b/test/regress/regress0/sygus/list-head-x.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --no-dump-synth
 (set-logic ALL_SUPPORTED)
 
 (declare-datatypes () ((List (cons (head Int) (tail List)) (nil))))

diff --git a/test/regress/regress0/sygus/max.sy b/test/regress/regress0/sygus/max.sy
index dec4594d7b4ab3399b2a147ee751d96329007103..e6e3de5fc91c44011a3659987d7ab4f7e739b7eb 100644 (file)
--- a/test/regress/regress0/sygus/max.sy
+++ b/test/regress/regress0/sygus/max.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --no-dump-synth
 (set-logic LIA)
 
 (synth-fun max ((x Int) (y Int)) Int

diff --git a/test/regress/regress0/sygus/max2-univ.sy b/test/regress/regress0/sygus/max2-univ.sy
index 3f8aac3b274ec7203a98c7fe31ff6d9d841d3fa6..927148d81178390f03105a1945efacfd94d9032c 100644 (file)
--- a/test/regress/regress0/sygus/max2-univ.sy
+++ b/test/regress/regress0/sygus/max2-univ.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi --no-dump-synth
+; COMMAND-LINE: --no-dump-synth
 ; Synthesize the maximum of 2 integers, but property has 4 variables (requires 2 passes)
 (set-logic LIA)
 (synth-fun max2 ((x Int) (y Int)) Int)

diff --git a/test/regress/regress0/sygus/multi-fun-polynomial2.sy b/test/regress/regress0/sygus/multi-fun-polynomial2.sy
index 6d185ba3f79296a42322bca9aa944d7020fbacf7..c238de5ddf3b69030316c4ee5c64228e4f663686 100644 (file)
--- a/test/regress/regress0/sygus/multi-fun-polynomial2.sy
+++ b/test/regress/regress0/sygus/multi-fun-polynomial2.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi --no-dump-synth
+; COMMAND-LINE: --no-dump-synth
 
 (set-logic LIA)
 
@@ -32,4 +32,4 @@
 
 (check-synth)
 
-; (x, y), (x-y, 0) ... are valid solutions
\ No newline at end of file
+; (x, y), (x-y, 0) ... are valid solutions

diff --git a/test/regress/regress0/sygus/nflat-fwd-3.sy b/test/regress/regress0/sygus/nflat-fwd-3.sy
index 9065a1025e2388858d8a60dcf39111de12f61f38..d3624a731306bec07f82ec56cad9e544bc38b92e 100644 (file)
--- a/test/regress/regress0/sygus/nflat-fwd-3.sy
+++ b/test/regress/regress0/sygus/nflat-fwd-3.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si --no-dump-synth
+; COMMAND-LINE: --no-dump-synth
 (set-logic LIA)
 (synth-fun f ((x Int)) Int
     ((Start Int ((+ (+ Con Con) Con) x))

diff --git a/test/regress/regress0/sygus/nflat-fwd.sy b/test/regress/regress0/sygus/nflat-fwd.sy
index d211d475bf927cfca1cec34316936e8a3e00eadb..3f15d59151ce272929b8b8f577a9ad74379b5382 100644 (file)
--- a/test/regress/regress0/sygus/nflat-fwd.sy
+++ b/test/regress/regress0/sygus/nflat-fwd.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi --no-dump-synth
+; COMMAND-LINE: --no-dump-synth
 (set-logic LIA)
 (synth-fun f ((x Int)) Int
     ((Start Int ((+ Con Con) (+ (+ Start Start) Con) x))

diff --git a/test/regress/regress0/sygus/no-flat-simp.sy b/test/regress/regress0/sygus/no-flat-simp.sy
index cb284b18093ede6663c664267ae5739c554ed3ee..af1284f133e9a03509b8b449927266e70e68d080 100644 (file)
--- a/test/regress/regress0/sygus/no-flat-simp.sy
+++ b/test/regress/regress0/sygus/no-flat-simp.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si --no-dump-synth
+; COMMAND-LINE: --no-dump-synth
 
 (set-logic LIA)
 

diff --git a/test/regress/regress0/sygus/no-mention.sy b/test/regress/regress0/sygus/no-mention.sy
index 05dfbced393b7070c06ae09b1a22c32daa2b967c..60efc1b74df87fa7cecd5639922f9033539ae87b 100644 (file)
--- a/test/regress/regress0/sygus/no-mention.sy
+++ b/test/regress/regress0/sygus/no-mention.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi --no-dump-synth
+; COMMAND-LINE: --no-dump-synth
 (set-logic LIA)
 
 (synth-fun p ((x Int) (y Int)) Int)

diff --git a/test/regress/regress0/sygus/no-syntax-test-bool.sy b/test/regress/regress0/sygus/no-syntax-test-bool.sy
index 4b3fa22e6328234800f54c7a6c6fc922d305ebd4..ee27b30eb12ba18e854f9e7bff46881373831c8f 100644 (file)
--- a/test/regress/regress0/sygus/no-syntax-test-bool.sy
+++ b/test/regress/regress0/sygus/no-syntax-test-bool.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si --no-dump-synth
+; COMMAND-LINE: --no-dump-synth
 
 (set-logic LIA)
 

diff --git a/test/regress/regress0/sygus/no-syntax-test-no-si.sy b/test/regress/regress0/sygus/no-syntax-test-no-si.sy
index 86b60638b24e86b7a5cf08b06751299f84ed5ecb..bd8da19008726a76655f9ec03de1b2d06736dbf4 100644 (file)
--- a/test/regress/regress0/sygus/no-syntax-test-no-si.sy
+++ b/test/regress/regress0/sygus/no-syntax-test-no-si.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi --no-dump-synth
+; COMMAND-LINE: --no-dump-synth
 
 (set-logic LIA)
 

diff --git a/test/regress/regress0/sygus/no-syntax-test.sy b/test/regress/regress0/sygus/no-syntax-test.sy
index b95f31aa782cbec2adb32d1d1b387b3a1ebebb30..2b3d5f3e95f3465ffda5f514cb71c2108a9e68ae 100644 (file)
--- a/test/regress/regress0/sygus/no-syntax-test.sy
+++ b/test/regress/regress0/sygus/no-syntax-test.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si --no-dump-synth
+; COMMAND-LINE: --no-dump-synth
 
 (set-logic LIA)
 

diff --git a/test/regress/regress0/sygus/parity-AIG-d0.sy b/test/regress/regress0/sygus/parity-AIG-d0.sy
index 03d180634cd30927df002c6fded2a48b6dacf30e..3cc577bd8659e39d782afb3c9c404ef0447429cd 100644 (file)
--- a/test/regress/regress0/sygus/parity-AIG-d0.sy
+++ b/test/regress/regress0/sygus/parity-AIG-d0.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --no-dump-synth
 (set-logic BV)
 
 (define-fun parity ((a Bool) (b Bool) (c Bool) (d Bool)) Bool
@@ -27,4 +27,4 @@
 ;(not
 ;  (and
 ;   (and (not (and (not a) b)) (not (and d (not c))))
-;   (and (not (and (not b) a)) (not (and (not d) c)))))) 
\ No newline at end of file
+;   (and (not (and (not b) a)) (not (and (not d) c)))))) 

diff --git a/test/regress/regress0/sygus/strings-small.sy b/test/regress/regress0/sygus/strings-small.sy
index bc559f94a28e436eab6bce50cab5ed8efe9c32f2..40346bcdfb1f33e4fdd7060cc39999235787c9c0 100644 (file)
--- a/test/regress/regress0/sygus/strings-small.sy
+++ b/test/regress/regress0/sygus/strings-small.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si --no-dump-synth
+; COMMAND-LINE: --no-dump-synth
 (set-logic SLIA)
 (synth-fun f ((firstname String) (lastname String)) String
 ((Start String (ntString))

diff --git a/test/regress/regress0/sygus/sygus-dt.sy b/test/regress/regress0/sygus/sygus-dt.sy
index e842477e8e4f9c52370feebd570767e9f4840ebe..be67491399fe37e7e9e849d8985cdddb750a129b 100644 (file)
--- a/test/regress/regress0/sygus/sygus-dt.sy
+++ b/test/regress/regress0/sygus/sygus-dt.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi --no-dump-synth
+; COMMAND-LINE: --no-dump-synth
 
 (set-logic LIA)
 
@@ -13,4 +13,4 @@
 (declare-var x Int)
 
 (constraint (= (f x) (cons x nil)))
-(check-synth)
\ No newline at end of file
+(check-synth)

diff --git a/test/regress/regress0/sygus/tl-type.sy b/test/regress/regress0/sygus/tl-type.sy
index 1545f86cd4f21cda8fea8f733001827d1ea5f045..a6980425a4372044fb00dd7fe72cad84f0f3afad 100644 (file)
--- a/test/regress/regress0/sygus/tl-type.sy
+++ b/test/regress/regress0/sygus/tl-type.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi --no-cegqi-si --no-dump-synth
+; COMMAND-LINE: --cegqi-si=none --no-dump-synth
 (set-logic LIA)
 (synth-fun f ((x Int)) Int
     ((Start Int (Term (+ Start Start)))

diff --git a/test/regress/regress0/sygus/twolets1.sy b/test/regress/regress0/sygus/twolets1.sy
index 7f84ce06c2f40bad8e457f6a957a4b0796436351..b016872b4ab94e8e69a45a89beeb15e2f6d1c4f3 100644 (file)
--- a/test/regress/regress0/sygus/twolets1.sy
+++ b/test/regress/regress0/sygus/twolets1.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --no-dump-synth
 (set-logic LIA)
 
 ;; f1 is x plus 2 ;; f2 is 2x plus 5

diff --git a/test/regress/regress0/sygus/twolets2-orig.sy b/test/regress/regress0/sygus/twolets2-orig.sy
index 91bab5ece8d48d087b41a4f24d9c520a92d29557..70d1ffa0248cf21342ff55e4df1c405ad9190705 100644 (file)
--- a/test/regress/regress0/sygus/twolets2-orig.sy
+++ b/test/regress/regress0/sygus/twolets2-orig.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --no-dump-synth
 (set-logic LIA)
 (synth-fun f1 ((x Int)) Int
      (

diff --git a/test/regress/regress0/sygus/uminus_one.sy b/test/regress/regress0/sygus/uminus_one.sy
index 9886f6a7b16b38c895a10abeee0c7ab6eae1f1ef..e98be942b3d4abfd47fd584afa321e97d4d5018e 100644 (file)
--- a/test/regress/regress0/sygus/uminus_one.sy
+++ b/test/regress/regress0/sygus/uminus_one.sy
@@ -1,7 +1,7 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi --no-dump-synth
+; COMMAND-LINE: --no-dump-synth
 (set-logic LIA)
 (synth-fun f ((x Int)) Int ((Start Int ((- 1)))))
 (declare-var x Int)
 (constraint (= (f x) (- 1)))
-(check-synth)
\ No newline at end of file
+(check-synth)

diff --git a/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy b/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy
index 7c9d6c6012f3423bf18bc40f4baf6e216e9a2499..300b6b65cd4af87ff5526ec1414ffeca8438af8f 100644 (file)
--- a/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy
+++ b/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi --no-dump-synth
+; COMMAND-LINE: --no-dump-synth
 
 (set-logic LIA)
 (synth-fun inv ((x Int)) Bool