Merge branch 'origin' of https://github.com/CVC4/CVC4.git

Conflicts:
	src/options/quantifiers_options

1 files changed, 33 insertions, 27 deletions

diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index 71bf7c426..54415d974 100755
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -767,7 +767,7 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) {
       Assert( dt.isSygus() );
       //get the solution
       Node sol;
-      int status;
+      int status = -1;
       if( d_last_inst_si ){
         Assert( d_conj->getCegConjectureSingleInv() != NULL );
         sol = d_conj->getSingleInvocationSolution( i, tn, status );
@@ -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;