From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 1 Sep 2016 21:35:06 +0000 (-0500)
Subject: Fix boolean term issue in invariants from sygus. Minor default options changes for... 
X-Git-Tag: cvc5-1.0.0~6028^2~64
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cbfc0961327831dc43ce6dda600740bab224ff6c;p=cvc5.git

Fix boolean term issue in invariants from sygus. Minor default options changes for cbqi.
---

diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index f5561ad23..f99333de2 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -301,9 +301,9 @@ option cbqiMidpoint --cbqi-midpoint bool :default false
   choose substitutions based on midpoints of lower and upper bounds for counterexample-based quantifier instantiation
 option cbqiNopt --cbqi-nopt bool :default true
   non-optimal bounds for counterexample-based quantifier instantiation
-option cbqiLitDepend --cbqi-lit-dep bool :default false
+option cbqiLitDepend --cbqi-lit-dep bool :default true
   dependency lemmas for quantifier alternation in counterexample-based quantifier instantiation
-option cbqiInnermost --cbqi-innermost bool :read-write :default false
+option cbqiInnermost --cbqi-innermost bool :read-write :default true
  only process innermost quantified formulas in counterexample-based quantifier instantiation
 option cbqiNestedQE --cbqi-nested-qe bool :default false
  process nested quantified formulas with quantifier elimination in counterexample-based quantifier instantiation
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index 71bf7c426..718d06c32 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -786,39 +786,45 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) {
             for( unsigned j=0; j<svl.getNumChildren(); j++ ){
               subs.push_back( Node::fromExpr( svl[j] ) );
             }
+            bool templIsPost = false;
+            Node templ;
             if( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_PRE ){
-              const CegConjectureSingleInv* ceg_si =
-                  d_conj->getCegConjectureSingleInv();
+              const CegConjectureSingleInv* ceg_si = d_conj->getCegConjectureSingleInv();
               if(ceg_si->d_trans_pre.find( prog ) != ceg_si->d_trans_pre.end()){
-                std::vector<Node>& templ_vars = d_conj->getProgTempVars(prog);
-                Assert(templ_vars.size() == subs.size());
-                Node pre = ceg_si->getTransPre(prog);
-                pre = pre.substitute( templ_vars.begin(), templ_vars.end(),
-                                      subs.begin(), subs.end() );
-                TermDbSygus* sygusDb = getTermDatabase()->getTermDatabaseSygus();
-                sol = sygusDb->sygusToBuiltin( sol, sol.getType() );
-                Trace("cegqi-inv") << "Builtin version of solution is : "
-                                   << sol << ", type : " << sol.getType()
-                                   << std::endl;
-                sol = NodeManager::currentNM()->mkNode( OR, sol, pre );
+                templ = ceg_si->getTransPre(prog);
+                templIsPost = false;
               }
             }else if(options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_POST){
-              const CegConjectureSingleInv* ceg_si =
-                  d_conj->getCegConjectureSingleInv();
+              const CegConjectureSingleInv* ceg_si = d_conj->getCegConjectureSingleInv();
               if(ceg_si->d_trans_post.find(prog) != ceg_si->d_trans_post.end()){
-                std::vector<Node>& templ_vars = d_conj->getProgTempVars(prog);
-                Assert( templ_vars.size()==subs.size() );
-                Node post = ceg_si->getTransPost(prog);
-                post = post.substitute( templ_vars.begin(), templ_vars.end(),
-                                        subs.begin(), subs.end() );
-                TermDbSygus* sygusDb = getTermDatabase()->getTermDatabaseSygus();
-                sol = sygusDb->sygusToBuiltin( sol, sol.getType() );
-                Trace("cegqi-inv") << "Builtin version of solution is : "
-                                   << sol << ", type : " << sol.getType()
-                                   << std::endl;
-                sol = NodeManager::currentNM()->mkNode( AND, sol, post );
+                templ = ceg_si->getTransPost(prog);
+                templIsPost = true;
               }
             }
+            if( !templ.isNull() ){
+              std::vector<Node>& templ_vars = d_conj->getProgTempVars(prog);
+              
+              //take into consideration Boolean term conversion (this step can be eliminated when boolean term conversion is eliminated)
+              std::vector< Node > vars;
+              vars.insert( vars.end(), templ_vars.begin(), templ_vars.end() );
+              Node vl = Node::fromExpr( dt.getSygusVarList() );
+              Assert(vars.size() == subs.size());
+              for( unsigned j=0; j<templ_vars.size(); j++ ){
+                if( vl[j].getType().isBoolean() ){
+                  Node c = NodeManager::currentNM()->mkConst(BitVector(1u, 1u));
+                  vars[j] = vars[j].eqNode( c );
+                }
+                Assert( vars[j].getType()==subs[j].getType() );
+              }
+              
+              templ = templ.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+              TermDbSygus* sygusDb = getTermDatabase()->getTermDatabaseSygus();
+              sol = sygusDb->sygusToBuiltin( sol, sol.getType() );
+              Trace("cegqi-inv") << "Builtin version of solution is : "
+                                 << sol << ", type : " << sol.getType()
+                                 << std::endl;
+              sol = NodeManager::currentNM()->mkNode( templIsPost ? AND : OR, sol, templ );
+            }
             if( sol==sygus_sol ){
               sol = sygus_sol;
               status = 1;
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index 71c0858bf..2c0e0a32f 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -427,6 +427,8 @@ Node InstStrategyCbqi::doNestedQERec( Node q, Node n, std::map< Node, Node >& vi
             d_nested_qe_info[nr].d_inst_terms.clear();
             d_nested_qe_info[nr].d_inst_terms.insert( d_nested_qe_info[nr].d_inst_terms.end(), inst_terms.begin(), inst_terms.end() );
             d_nested_qe_info[nr].d_doVts = doVts;
+            //TODO: ensure this holds by restricting prenex when cbqiNestedQe is true.
+            Assert( !options::cbqiInnermost() );
           }
         } 
       }