Minor: Ensure indexed terms are in EE. Add support for bv constants in sygus parser.

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 320fead5f11a7b55dce2cdf68cc6ebdc6d58dfc1..67f26533edf2d91d59e58ac037000d56c748ae08 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -640,7 +640,8 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
           const DatatypeConstructor& ctor = dt[j];
           std::vector<Expr> bvs, extraArgs;
           for(size_t k = 0; k < ctor.getNumArgs(); ++k) {
-            Expr bv = EXPR_MANAGER->mkBoundVar(ctor[k].getName(), SelectorType(ctor[k].getType()).getRangeType());
+            std::string vname = "v_" + ctor[k].getName();
+            Expr bv = EXPR_MANAGER->mkBoundVar(vname, SelectorType(ctor[k].getType()).getRangeType());
             bvs.push_back(bv);
             extraArgs.push_back(bv);
           }
@@ -757,11 +758,25 @@ sygusGTerm[CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops]
     { assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 );
       std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2);
       ops.push_back(MK_CONST( BitVector(hexString, 16) ));
+      name = dt.getName() + "_" + AntlrInput::tokenText($HEX_LITERAL);
+      std::string testerId("is-");
+      testerId.append(name);
+      PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE);
+      PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE);
+      CVC4::DatatypeConstructor c(name, testerId);
+      dt.addConstructor(c);
     }
   | BINARY_LITERAL
     { assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 );
       std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2);
       ops.push_back(MK_CONST( BitVector(binString, 2) ));
+      name = dt.getName() + "_" + AntlrInput::tokenText($BINARY_LITERAL);
+      std::string testerId("is-");
+      testerId.append(name);
+      PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE);
+      PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE);
+      CVC4::DatatypeConstructor c(name, testerId);
+      dt.addConstructor(c);
     }
   | symbol[name,CHECK_DECLARED,SYM_VARIABLE]
     { Expr bv = PARSER_STATE->getVariable(name);

diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index bf9409f064e08cf23a6f7bef03e8007c22e55b91..1b02b2a13def594e1224e322085676bb229f117e 100644 (file)
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -89,7 +89,7 @@ bool CegInstantiation::needsModel( Theory::Effort e ) {
   return true;
 }
 bool CegInstantiation::needsFullModel( Theory::Effort e ) {
-  return false;
+  return true;
 }
 
 void CegInstantiation::check( Theory::Effort e, unsigned quant_e ) {
@@ -234,9 +234,9 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
           Assert( inst.getKind()==NOT );
           Assert( inst[0].getKind()==FORALL );
           //immediately skolemize
-          Node inst_sk = getTermDatabase()->getSkolemizedBody( inst[0] );
+          Node inst_sk = getTermDatabase()->getSkolemizedBody( inst[0] ).negate();
           Trace("cegqi-lemma") << "Counterexample lemma : " << inst_sk << std::endl;
-          d_quantEngine->addLemma( NodeManager::currentNM()->mkNode( OR, q.negate(), inst_sk.negate() ) );
+          d_quantEngine->addLemma( NodeManager::currentNM()->mkNode( OR, q.negate(), inst_sk ) );
           conj->d_ce_sk.push_back( inst[0] );
           Trace("cegqi-engine") << "  ...find counterexample." << std::endl;
         }

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 34c40c8c4d383634a1f67779b92cc6ea7eca6be1..be58919db01eec660aee9f864fdad8b49fed5265 100644 (file)
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -396,11 +396,11 @@ void TermDb::reset( Theory::Effort effort ){
   d_func_map_trie.clear();
   d_func_map_eqc_trie.clear();
 
+  eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine(); 
   //compute has map
   if( options::termDbMode()==TERM_DB_RELEVANT ){
     d_has_map.clear();
     d_has_eqc.clear();
-    eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
     eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
     while( !eqcs_i.isFinished() ){
       TNode r = (*eqcs_i);
@@ -428,7 +428,6 @@ void TermDb::reset( Theory::Effort effort ){
       if (theory && d_quantEngine->getTheoryEngine()->d_logicInfo.isTheoryEnabled(theoryId)) {
         context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end();
         for (unsigned i = 0; it != it_end; ++ it, ++i) {
-          Trace("ajr-temp") << "Set has term " << (*it).assertion << std::endl;
           setHasTerm( (*it).assertion );
         }
       }
@@ -439,32 +438,40 @@ void TermDb::reset( Theory::Effort effort ){
   //rebuild d_func/pred_map_trie for each operation, this will calculate all congruent terms
   for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){
     d_op_nonred_count[ it->first ] = 0;
-    if( !it->second.empty() ){
-      for( unsigned i=0; i<it->second.size(); i++ ){
-        Node n = it->second[i];
-        if( hasTermCurrent( n ) ){
-          if( !n.getAttribute(NoMatchAttribute()) ){
-            if( options::finiteModelFind() ){
-              computeModelBasisArgAttribute( n );
-            }
-            computeArgReps( n );
-            if( !d_func_map_trie[ it->first ].addTerm( n, d_arg_reps[n] ) ){
-              NoMatchAttribute nma;
-              n.setAttribute(nma,true);
-              Trace("term-db-stats-debug") << n << " is redundant." << std::endl;
-              congruentCount++;
-            }else{
-              nonCongruentCount++;
-              d_op_nonred_count[ it->first ]++;
+    Trace("term-db-debug") << "Adding terms for operator " << it->first << std::endl;
+    for( unsigned i=0; i<it->second.size(); i++ ){
+      Node n = it->second[i];
+      if( hasTermCurrent( n ) && ee->hasTerm( n ) ){
+        if( !n.getAttribute(NoMatchAttribute()) ){
+          if( options::finiteModelFind() ){
+            computeModelBasisArgAttribute( n );
+          }
+          computeArgReps( n );
+          
+          if( Trace.isOn("term-db-debug") ){
+            Trace("term-db-debug") << "Adding term " << n << " with arg reps : ";
+            for( unsigned i=0; i<d_arg_reps[n].size(); i++ ){
+              Trace("term-db-debug") << d_arg_reps[n] << " ";
             }
-          }else{
+            Trace("term-db-debug") << std::endl;
+          }
+          
+          if( !d_func_map_trie[ it->first ].addTerm( n, d_arg_reps[n] ) ){
+            NoMatchAttribute nma;
+            n.setAttribute(nma,true);
+            Trace("term-db-debug") << n << " is redundant." << std::endl;
             congruentCount++;
-            alreadyCongruentCount++;
+          }else{
+            nonCongruentCount++;
+            d_op_nonred_count[ it->first ]++;
           }
         }else{
-          Trace("term-db-stats-debug") << n << " is not relevant." << std::endl;
-          nonRelevantCount++;
+          congruentCount++;
+          alreadyCongruentCount++;
         }
+      }else{
+        Trace("term-db-debug") << n << " is not relevant." << std::endl;
+        nonRelevantCount++;
       }
     }
   }

diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index 05fea6b5e23ba6f9045a3142110ca57dfc4e447f..9cb2b5b53972e1418bd007de5ec3deee41fa1575 100644 (file)
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -1539,7 +1539,8 @@ void StrongSolverTheoryUF::ensureEqcRec( Node n ) {
 
 /** has eqc */
 bool StrongSolverTheoryUF::hasEqc( Node a ) {
-  return d_rel_eqc.find( a )!=d_rel_eqc.end() && d_rel_eqc[a];
+  NodeBoolMap::iterator it = d_rel_eqc.find( a );
+  return it!=d_rel_eqc.end() && (*it).second;
 }
 
 /** new node */