From: ajreynol Date: Fri, 16 Jan 2015 08:29:15 +0000 (+0100) Subject: Minor: Ensure indexed terms are in EE. Add support for bv constants in sygus parser. X-Git-Tag: cvc5-1.0.0~6441 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=338ec2ee86e16423b265ba9bfc036606223f846f;p=cvc5.git 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 320fead5f..67f26533e 100644 --- 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 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& 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 bf9409f06..1b02b2a13 100644 --- 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 34c40c8c4..be58919db 100644 --- 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::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; isecond.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; isecond.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; ifirst ].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 05fea6b5e..9cb2b5b53 100644 --- 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 */