diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-07-20 19:46:21 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-07-20 19:46:21 +0200 |
commit | f62d9456b41bf17df1d339e46776c9213cb3705a (patch) | |
tree | 01d3448b3c9fe89ead56c72b18f8516292092e13 /src/theory | |
parent | 7943953741c67d8246f983e193d26812d959b4cd (diff) |
Squashed merge of SygusComp 2015 branch.
Diffstat (limited to 'src/theory')
22 files changed, 596 insertions, 96 deletions
diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index b4ecc1d3d..3cbc45cd1 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -70,6 +70,9 @@ operator BITVECTOR_SLE 2 "bit-vector signed less than or equal (the two bit-vect operator BITVECTOR_SGT 2 "bit-vector signed greater than (the two bit-vector parameters must have same width)" operator BITVECTOR_SGE 2 "bit-vector signed greater than or equal (the two bit-vector parameters must have same width)" +operator BITVECTOR_REDOR 1 "bit-vector redor" +operator BITVECTOR_REDAND 1 "bit-vector redand" + operator BITVECTOR_EAGER_ATOM 1 "formula to be treated as a bv atom via eager bit-blasting (internal-only symbol)" operator BITVECTOR_ACKERMANIZE_UDIV 1 "term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvudiv (internal-only symbol)" operator BITVECTOR_ACKERMANIZE_UREM 1 "term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvurem (internal-only symbol)" @@ -171,6 +174,10 @@ typerule BITVECTOR_SLE ::CVC4::theory::bv::BitVectorPredicateTypeRule typerule BITVECTOR_SGT ::CVC4::theory::bv::BitVectorPredicateTypeRule typerule BITVECTOR_SGE ::CVC4::theory::bv::BitVectorPredicateTypeRule +typerule BITVECTOR_REDOR ::CVC4::theory::bv::BitVectorUnaryPredicateTypeRule +typerule BITVECTOR_REDAND ::CVC4::theory::bv::BitVectorUnaryPredicateTypeRule + + typerule BITVECTOR_EAGER_ATOM ::CVC4::theory::bv::BitVectorEagerAtomTypeRule typerule BITVECTOR_ACKERMANIZE_UDIV ::CVC4::theory::bv::BitVectorAckermanizationUdivTypeRule typerule BITVECTOR_ACKERMANIZE_UREM ::CVC4::theory::bv::BitVectorAckermanizationUremTypeRule diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index 3cc1c323c..768923ee6 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -49,6 +49,8 @@ enum RewriteRuleId { UgeEliminate, SgeEliminate, SgtEliminate, + RedorEliminate, + RedandEliminate, SubEliminate, SltEliminate, SleEliminate, @@ -188,6 +190,8 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { case SgtEliminate: out << "SgtEliminate"; return out; case UgeEliminate: out << "UgeEliminate"; return out; case SgeEliminate: out << "SgeEliminate"; return out; + case RedorEliminate: out << "RedorEliminate"; return out; + case RedandEliminate: out << "RedandEliminate"; return out; case RepeatEliminate: out << "RepeatEliminate"; return out; case RotateLeftEliminate: out << "RotateLeftEliminate"; return out; case RotateRightEliminate:out << "RotateRightEliminate";return out; @@ -522,6 +526,8 @@ struct AllRewriteRules { RewriteRule<UltPlusOne> rule119; RewriteRule<ConcatToMult> rule120; RewriteRule<IsPowerOfTwo> rule121; + RewriteRule<RedorEliminate> rule122; + RewriteRule<RedandEliminate> rule123; }; template<> inline diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h index 0442c47d9..cd173a6dd 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h +++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h @@ -479,6 +479,33 @@ Node RewriteRule<SignExtendEliminate>::apply(TNode node) { return utils::mkConcat(extension, node[0]); } +template<> +bool RewriteRule<RedorEliminate>::applies(TNode node) { + return (node.getKind() == kind::BITVECTOR_REDOR); +} + +template<> +Node RewriteRule<RedorEliminate>::apply(TNode node) { + Debug("bv-rewrite") << "RewriteRule<RedorEliminate>(" << node << ")" << std::endl; + TNode a = node[0]; + unsigned size = utils::getSize(node[0]); + Node result = NodeManager::currentNM()->mkNode(kind::EQUAL, a, utils::mkConst( size, 0 ) ); + return result.negate(); +} + +template<> +bool RewriteRule<RedandEliminate>::applies(TNode node) { + return (node.getKind() == kind::BITVECTOR_REDAND); +} + +template<> +Node RewriteRule<RedandEliminate>::apply(TNode node) { + Debug("bv-rewrite") << "RewriteRule<RedandEliminate>(" << node << ")" << std::endl; + TNode a = node[0]; + unsigned size = utils::getSize(node[0]); + Node result = NodeManager::currentNM()->mkNode(kind::EQUAL, a, utils::mkOnes( size ) ); + return result; +} } } diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index 86f2c6760..f2adea411 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -553,6 +553,22 @@ RewriteResponse TheoryBVRewriter::RewriteRotateLeft(TNode node, bool prerewrite) return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); } +RewriteResponse TheoryBVRewriter::RewriteRedor(TNode node, bool prerewrite){ + Node resultNode = LinearRewriteStrategy + < RewriteRule<RedorEliminate> + >::apply(node); + + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); +} + +RewriteResponse TheoryBVRewriter::RewriteRedand(TNode node, bool prerewrite){ + Node resultNode = LinearRewriteStrategy + < RewriteRule<RedandEliminate> + >::apply(node); + + return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); +} + RewriteResponse TheoryBVRewriter::RewriteBVToNat(TNode node, bool prerewrite) { Node resultNode = LinearRewriteStrategy < RewriteRule<BVToNatEliminate> @@ -651,6 +667,8 @@ void TheoryBVRewriter::initializeRewrites() { d_rewriteTable [ kind::BITVECTOR_SIGN_EXTEND ] = RewriteSignExtend; d_rewriteTable [ kind::BITVECTOR_ROTATE_RIGHT ] = RewriteRotateRight; d_rewriteTable [ kind::BITVECTOR_ROTATE_LEFT ] = RewriteRotateLeft; + d_rewriteTable [ kind::BITVECTOR_REDOR ] = RewriteRedor; + d_rewriteTable [ kind::BITVECTOR_REDAND ] = RewriteRedand; d_rewriteTable [ kind::BITVECTOR_TO_NAT ] = RewriteBVToNat; d_rewriteTable [ kind::INT_TO_BITVECTOR ] = RewriteIntToBV; diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h index 42bccb534..3f0fa8194 100644 --- a/src/theory/bv/theory_bv_rewriter.h +++ b/src/theory/bv/theory_bv_rewriter.h @@ -77,6 +77,8 @@ class TheoryBVRewriter { static RewriteResponse RewriteSignExtend(TNode node, bool prerewrite = false); static RewriteResponse RewriteRotateRight(TNode node, bool prerewrite = false); static RewriteResponse RewriteRotateLeft(TNode node, bool prerewrite = false); + static RewriteResponse RewriteRedor(TNode node, bool prerewrite = false); + static RewriteResponse RewriteRedand(TNode node, bool prerewrite = false); static RewriteResponse RewriteBVToNat(TNode node, bool prerewrite = false); static RewriteResponse RewriteIntToBV(TNode node, bool prerewrite = false); diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h index 81a2d9a27..fbb285fe0 100644 --- a/src/theory/bv/theory_bv_type_rules.h +++ b/src/theory/bv/theory_bv_type_rules.h @@ -112,6 +112,20 @@ public: } };/* class BitVectorPredicateTypeRule */ +class BitVectorUnaryPredicateTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + if( check ) { + TypeNode type = n[0].getType(check); + if (!type.isBitVector()) { + throw TypeCheckingExceptionPrivate(n, "expecting bit-vector terms"); + } + } + return nodeManager->booleanType(); + } +};/* class BitVectorUnaryPredicateTypeRule */ + class BitVectorEagerAtomTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index 6ebc9db92..a8b6887e5 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -385,6 +385,8 @@ inline bool isBVPredicate(TNode node) { node.getKind() == kind::BITVECTOR_SGE || node.getKind() == kind::BITVECTOR_ULE || node.getKind() == kind::BITVECTOR_SLE || + node.getKind() == kind::BITVECTOR_REDOR || + node.getKind() == kind::BITVECTOR_REDAND || ( node.getKind() == kind::NOT && (node[0].getKind() == kind::EQUAL || node[0].getKind() == kind::BITVECTOR_ULT || node[0].getKind() == kind::BITVECTOR_SLT || @@ -393,7 +395,9 @@ inline bool isBVPredicate(TNode node) { node[0].getKind() == kind::BITVECTOR_SGT || node[0].getKind() == kind::BITVECTOR_SGE || node[0].getKind() == kind::BITVECTOR_ULE || - node[0].getKind() == kind::BITVECTOR_SLE))) + node[0].getKind() == kind::BITVECTOR_SLE || + node[0].getKind() == kind::BITVECTOR_REDOR || + node[0].getKind() == kind::BITVECTOR_REDAND))) { return true; } diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index a8121b67d..3ab29f334 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -650,12 +650,22 @@ void SygusSymBreak::addTester( Node tst ) { std::map< Node, ProgSearch * >::iterator it = d_prog_search.find( a ); ProgSearch * ps; if( it==d_prog_search.end() ){ - ps = new ProgSearch( this, a, d_context ); + //check if sygus type + TypeNode tn = a.getType(); + Assert( DatatypesRewriter::isTypeDatatype( tn ) ); + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + if( dt.isSygus() ){ + ps = new ProgSearch( this, a, d_context ); + }else{ + ps = NULL; + } d_prog_search[a] = ps; }else{ ps = it->second; } - ps->addTester( tst ); + if( ps ){ + ps->addTester( tst ); + } } } @@ -781,7 +791,7 @@ bool SygusSymBreak::ProgSearch::processSubprograms( Node n, int depth, int odept Node SygusSymBreak::ProgSearch::getCandidateProgramAtDepth( int depth, Node prog, int curr_depth, Node parent, std::map< TypeNode, int >& var_count, std::vector< Node >& testers, std::map< Node, std::vector< Node > >& testers_u ) { Assert( depth>=curr_depth ); - Trace("sygus-sym-break-debug") << "Reconstructing program for " << prog << " at depth " << curr_depth << "/" << depth << std::endl; + Trace("sygus-sym-break-debug") << "Reconstructing program for " << prog << " at depth " << curr_depth << "/" << depth << " " << prog.getType() << std::endl; NodeMap::const_iterator it = d_testers.find( prog ); if( it!=d_testers.end() ){ Node tst = (*it).second; @@ -823,7 +833,7 @@ bool SygusSymBreak::processCurrentProgram( Node a, TypeNode at, int depth, Node int tsize = d_tds->getSygusTermSize( prog ); if( itnp==d_normalized_to_orig[at].end() ){ d_normalized_to_orig[at][progr] = prog; - if( progr.getKind()==SKOLEM && d_tds->getSygusType( progr )==at ){ + if( progr.getKind()==SKOLEM && d_tds->getSygusTypeForVar( progr )==at ){ Trace("sygus-nf") << "* Sygus sym break : " << prog << " rewrites to variable " << progr << " of same type as self" << std::endl; d_redundant[at][prog] = true; red = true; diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index 5f3498f49..045407bf0 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -70,7 +70,7 @@ void CegConjecture::assign( QuantifiersEngine * qe, Node q ) { } void CegConjecture::initializeGuard( QuantifiersEngine * qe ){ - if( d_guard.isNull() ){ + if( isAssigned() && d_guard.isNull() ){ d_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G", NodeManager::currentNM()->booleanType() ) ); //specify guard behavior d_guard = qe->getValuation().ensureLiteral( d_guard ); @@ -137,6 +137,10 @@ bool CegConjecture::isSingleInvocation() { return d_ceg_si->isSingleInvocation(); } +bool CegConjecture::needsCheck() { + return d_active && !d_infeasible && ( !isSingleInvocation() || d_ceg_si->needsCheck() ); +} + CegInstantiation::CegInstantiation( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ){ d_conj = new CegConjecture( qe->getSatContext() ); d_last_inst_si = false; @@ -155,7 +159,7 @@ void CegInstantiation::check( Theory::Effort e, unsigned quant_e ) { Trace("cegqi-engine") << "---Counterexample Guided Instantiation Engine---" << std::endl; Trace("cegqi-engine-debug") << std::endl; Trace("cegqi-engine-debug") << "Current conjecture status : active : " << d_conj->d_active << " feasible : " << !d_conj->d_infeasible << std::endl; - if( d_conj->d_active && !d_conj->d_infeasible ){ + if( d_conj->needsCheck() ){ checkCegConjecture( d_conj ); } Trace("cegqi-engine") << "Finished Counterexample Guided Instantiation engine." << std::endl; @@ -213,29 +217,32 @@ void CegInstantiation::assertNode( Node n ) { } Node CegInstantiation::getNextDecisionRequest() { - d_conj->initializeGuard( d_quantEngine ); - bool value; - if( !d_quantEngine->getValuation().hasSatValue( d_conj->d_guard, value ) ) { - //if( d_conj->d_guard_split.isNull() ){ - // Node lem = NodeManager::currentNM()->mkNode( OR, d_conj->d_guard.negate(), d_conj->d_guard ); - // d_quantEngine->getOutputChannel().lemma( lem ); - //} - Trace("cegqi-debug") << "CEGQI : Decide next on : " << d_conj->d_guard << "..." << std::endl; - return d_conj->d_guard; - } //enforce fairness - if( d_conj->isAssigned() && d_conj->getCegqiFairMode()!=CEGQI_FAIR_NONE ){ - Node lit = d_conj->getLiteral( d_quantEngine, d_conj->d_curr_lit.get() ); - if( d_quantEngine->getValuation().hasSatValue( lit, value ) ) { - if( !value ){ - d_conj->d_curr_lit.set( d_conj->d_curr_lit.get() + 1 ); - lit = d_conj->getLiteral( d_quantEngine, d_conj->d_curr_lit.get() ); - Trace("cegqi-debug") << "CEGQI : Decide on next lit : " << lit << "..." << std::endl; + if( d_conj->isAssigned() ){ + d_conj->initializeGuard( d_quantEngine ); + bool value; + if( !d_quantEngine->getValuation().hasSatValue( d_conj->d_guard, value ) ) { + //if( d_conj->d_guard_split.isNull() ){ + // Node lem = NodeManager::currentNM()->mkNode( OR, d_conj->d_guard.negate(), d_conj->d_guard ); + // d_quantEngine->getOutputChannel().lemma( lem ); + //} + Trace("cegqi-debug") << "CEGQI : Decide next on : " << d_conj->d_guard << "..." << std::endl; + return d_conj->d_guard; + } + + if( d_conj->getCegqiFairMode()!=CEGQI_FAIR_NONE ){ + Node lit = d_conj->getLiteral( d_quantEngine, d_conj->d_curr_lit.get() ); + if( d_quantEngine->getValuation().hasSatValue( lit, value ) ) { + if( !value ){ + d_conj->d_curr_lit.set( d_conj->d_curr_lit.get() + 1 ); + lit = d_conj->getLiteral( d_quantEngine, d_conj->d_curr_lit.get() ); + Trace("cegqi-debug") << "CEGQI : Decide on next lit : " << lit << "..." << std::endl; + return lit; + } + }else{ + Trace("cegqi-debug") << "CEGQI : Decide on current lit : " << lit << "..." << std::endl; return lit; } - }else{ - Trace("cegqi-debug") << "CEGQI : Decide on current lit : " << lit << "..." << std::endl; - return lit; } } @@ -484,7 +491,8 @@ void CegInstantiation::getMeasureLemmas( Node n, Node v, std::vector< Node >& le } void CegInstantiation::printSynthSolution( std::ostream& out ) { - if( d_conj ){ + if( d_conj->isAssigned() ){ + Trace("cegqi-debug") << "Printing synth solution..." << std::endl; //if( !(Trace.isOn("cegqi-stats")) ){ // out << "Solution:" << std::endl; //} @@ -530,6 +538,8 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) { out << ")" << std::endl; } } + }else{ + Assert( false ); } } diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h index 74e9b0aba..5f393626c 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.h +++ b/src/theory/quantifiers/ce_guided_instantiation.h @@ -83,6 +83,8 @@ public: //for fairness CegqiFairMode getCegqiFairMode(); /** is single invocation */ bool isSingleInvocation(); + /** needs check */ + bool needsCheck(); }; diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index 0a434e4ca..b7bbf8a93 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -742,29 +742,38 @@ CegConjectureSingleInv::CegConjectureSingleInv( CegConjecture * p ) : d_parent( d_sol = NULL; d_c_inst_match_trie = NULL; d_cinst = NULL; + d_has_ites = true; } Node CegConjectureSingleInv::getSingleInvLemma( Node guard ) { if( !d_single_inv.isNull() ) { - Assert( d_single_inv.getKind()==FORALL ); d_single_inv_var.clear(); d_single_inv_sk.clear(); - for( unsigned i=0; i<d_single_inv[0].getNumChildren(); i++ ){ - std::stringstream ss; - ss << "k_" << d_single_inv[0][i]; - Node k = NodeManager::currentNM()->mkSkolem( ss.str(), d_single_inv[0][i].getType(), "single invocation function skolem" ); - d_single_inv_var.push_back( d_single_inv[0][i] ); - d_single_inv_sk.push_back( k ); - d_single_inv_sk_index[k] = i; + Node inst; + if( d_single_inv.getKind()==FORALL ){ + for( unsigned i=0; i<d_single_inv[0].getNumChildren(); i++ ){ + std::stringstream ss; + ss << "k_" << d_single_inv[0][i]; + Node k = NodeManager::currentNM()->mkSkolem( ss.str(), d_single_inv[0][i].getType(), "single invocation function skolem" ); + d_single_inv_var.push_back( d_single_inv[0][i] ); + d_single_inv_sk.push_back( k ); + d_single_inv_sk_index[k] = i; + } + inst = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() ); + }else{ + inst = d_single_inv; } - Node inst = d_single_inv[1].substitute( d_single_inv_var.begin(), d_single_inv_var.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() ); inst = TermDb::simpleNegate( inst ); Trace("cegqi-si") << "Single invocation initial lemma : " << inst << std::endl; //initialize the instantiator for this - CegqiOutputSingleInv * cosi = new CegqiOutputSingleInv( this ); - d_cinst = new CegInstantiator( d_qe, cosi ); - d_cinst->d_vars.insert( d_cinst->d_vars.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() ); + if( !d_single_inv_sk.empty() ){ + CegqiOutputSingleInv * cosi = new CegqiOutputSingleInv( this ); + d_cinst = new CegInstantiator( d_qe, cosi ); + d_cinst->d_vars.insert( d_cinst->d_vars.end(), d_single_inv_sk.begin(), d_single_inv_sk.end() ); + }else{ + d_cinst = NULL; + } return NodeManager::currentNM()->mkNode( OR, guard.negate(), inst ); }else{ @@ -790,6 +799,14 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) { std::map< Node, std::map< Node, bool > > contains; for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ progs.push_back( q[0][i] ); + //check whether all types have ITE + TypeNode tn = q[0][i].getType(); + d_qe->getTermDatabaseSygus()->registerSygusType( tn ); + if( !d_qe->getTermDatabaseSygus()->sygusToBuiltinType( tn ).isBoolean() ){ + if( !d_qe->getTermDatabaseSygus()->hasKind( tn, ITE ) ){ + d_has_ites = false; + } + } } //collect information about conjunctions bool singleInvocation = false; @@ -881,8 +898,10 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) { //construct the single invocation version of the property Trace("cegqi-si") << "Single invocation formula conjuncts are : " << std::endl; //std::vector< Node > si_conj; - Assert( !pbvs.empty() ); - Node pbvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, pbvs ); + Node pbvl; + if( !pbvs.empty() ){ + pbvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, pbvs ); + } for( std::map< Node, std::vector< Node > >::iterator it = children.begin(); it != children.end(); ++it ){ //should hold since we prevent miniscoping Assert( d_single_inv.isNull() ); @@ -978,9 +997,14 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) { if( singleInvocation ){ Node bd = conjuncts.size()==1 ? conjuncts[0] : NodeManager::currentNM()->mkNode( OR, conjuncts ); - d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, bd ); + if( pbvl.isNull() ){ + d_single_inv = bd; + }else{ + d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, bd ); + } Trace("cegqi-si-debug") << "...formula is : " << d_single_inv << std::endl; - if( options::eMatching.wasSetByUser() ){ + /* + if( options::eMatching() && options::eMatching.wasSetByUser() ){ Node bd = d_qe->getTermDatabase()->getInstConstantBody( d_single_inv ); std::vector< Node > patTerms; std::vector< Node > exclude; @@ -992,6 +1016,7 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) { } } } + */ } } } @@ -999,9 +1024,68 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) { if( !singleInvocation ){ Trace("cegqi-si") << "Property is not single invocation." << std::endl; if( options::cegqiSingleInvAbort() ){ - Message() << "Property is not single invocation." << std::endl; + Notice() << "Property is not single invocation." << std::endl; exit( 0 ); } + }else{ + if( options::cegqiSingleInvPreRegInst() && d_single_inv.getKind()==FORALL ){ + Trace("cegqi-si-presolve") << "Check " << d_single_inv << std::endl; + //at preregister time, add proxy of obvious instantiations up front, which helps learning during preprocessing + std::vector< Node > vars; + std::map< Node, std::vector< Node > > teq; + for( unsigned i=0; i<d_single_inv[0].getNumChildren(); i++ ){ + vars.push_back( d_single_inv[0][i] ); + teq[d_single_inv[0][i]].clear(); + } + collectPresolveEqTerms( d_single_inv[1], teq ); + std::vector< Node > terms; + std::vector< Node > conj; + getPresolveEqConjuncts( vars, terms, teq, d_single_inv, conj ); + + if( !conj.empty() ){ + Node lem = conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj ); + Node g = NodeManager::currentNM()->mkSkolem( "g", NodeManager::currentNM()->booleanType() ); + lem = NodeManager::currentNM()->mkNode( OR, g, lem ); + d_qe->getOutputChannel().lemma( lem, false, true ); + } + } + } +} + +void CegConjectureSingleInv::collectPresolveEqTerms( Node n, std::map< Node, std::vector< Node > >& teq ) { + if( n.getKind()==EQUAL ){ + for( unsigned i=0; i<2; i++ ){ + std::map< Node, std::vector< Node > >::iterator it = teq.find( n[i] ); + if( it!=teq.end() ){ + Node nn = n[ i==0 ? 1 : 0 ]; + if( std::find( it->second.begin(), it->second.end(), nn )==it->second.end() ){ + it->second.push_back( nn ); + Trace("cegqi-si-presolve") << " - " << n[i] << " = " << nn << std::endl; + } + } + } + } + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + collectPresolveEqTerms( n[i], teq ); + } +} + +void CegConjectureSingleInv::getPresolveEqConjuncts( std::vector< Node >& vars, std::vector< Node >& terms, + std::map< Node, std::vector< Node > >& teq, Node f, std::vector< Node >& conj ) { + if( conj.size()<1000 ){ + if( terms.size()==f[0].getNumChildren() ){ + Node c = f[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); + conj.push_back( c ); + }else{ + unsigned i = terms.size(); + Node v = f[0][i]; + terms.push_back( Node::null() ); + for( unsigned j=0; j<teq[v].size(); j++ ){ + terms[i] = teq[v][j]; + getPresolveEqConjuncts( vars, terms, teq, f, conj ); + } + terms.pop_back(); + } } } @@ -1171,8 +1255,7 @@ bool CegConjectureSingleInv::addLemma( Node n ) { } void CegConjectureSingleInv::check( std::vector< Node >& lems ) { - if( !d_single_inv.isNull() ) { - Assert( d_cinst!=NULL ); + if( !d_single_inv.isNull() && d_cinst!=NULL ) { d_curr_lemmas.clear(); //check if there are delta lemmas d_cinst->getDeltaLemmas( lems ); @@ -1186,20 +1269,61 @@ void CegConjectureSingleInv::check( std::vector< Node >& lems ) { } } -Node CegConjectureSingleInv::constructSolution( unsigned i, unsigned index ) { +Node CegConjectureSingleInv::constructSolution( std::vector< unsigned >& indices, unsigned i, unsigned index ) { Assert( index<d_inst.size() ); Assert( i<d_inst[index].size() ); + unsigned uindex = indices[index]; if( index==d_inst.size()-1 ){ - return d_inst[index][i]; + return d_inst[uindex][i]; }else{ - Node cond = d_lemmas_produced[index]; + Node cond = d_lemmas_produced[uindex]; cond = TermDb::simpleNegate( cond ); - Node ite1 = d_inst[index][i]; - Node ite2 = constructSolution( i, index+1 ); + Node ite1 = d_inst[uindex][i]; + Node ite2 = constructSolution( indices, i, index+1 ); return NodeManager::currentNM()->mkNode( ITE, cond, ite1, ite2 ); } } +//TODO: use term size? +struct sortSiInstanceIndices { + CegConjectureSingleInv* d_ccsi; + int d_i; + bool operator() (unsigned i, unsigned j) { + if( d_ccsi->d_inst[i][d_i].isConst() && !d_ccsi->d_inst[j][d_i].isConst() ){ + return true; + }else{ + return false; + } + } +}; + +/* +Node removeBooleanIte( Node n ){ + if( n.getKind()==ITE && n.getType().isBoolean() ){ + Node n1 = removeBooleanIte( n[1] ); + Node n2 = removeBooleanIte( n[2] ); + return NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, n[0], n1 ), + NodeManager::currentNM()->mkNode( AND, n[0].negate(), n2 ) ); + }else{ + bool childChanged = false; + std::vector< Node > children; + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + Node nn = removeBooleanIte( n[i] ); + children.push_back( nn ); + childChanged = childChanged || nn!=n[i]; + } + if( childChanged ){ + if( n.hasOperator() ){ + children.insert( children.begin(), n.getOperator() ); + } + return NodeManager::currentNM()->mkNode( n.getKind(), children ); + }else{ + return n; + } + } +} +*/ + Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int& reconstructed ){ Assert( d_sol!=NULL ); Assert( !d_lemmas_produced.empty() ); @@ -1225,7 +1349,21 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int& d_sol->d_varList.push_back( varList[i-1] ); } //construct the solution - Node s = constructSolution( sol_index, 0 ); + Trace("csi-sol") << "Sort solution return values " << sol_index << std::endl; + Assert( d_lemmas_produced.size()==d_inst.size() ); + std::vector< unsigned > indices; + for( unsigned i=0; i<d_lemmas_produced.size(); i++ ){ + Assert( sol_index<d_inst[i].size() ); + indices.push_back( i ); + } + //sort indices based on heuristic : currently, do all constant returns first (leads to simpler conditions) + // TODO : to minimize solution size, put the largest term last + sortSiInstanceIndices ssii; + ssii.d_ccsi = this; + ssii.d_i = sol_index; + std::sort( indices.begin(), indices.end(), ssii ); + Trace("csi-sol") << "Construct solution" << std::endl; + Node s = constructSolution( indices, sol_index, 0 ); s = s.substitute( vars.begin(), vars.end(), d_varList.begin(), d_varList.end() ); d_orig_solution = s; @@ -1242,6 +1380,10 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int& if( reconstructed==1 ){ Trace("csi-sol") << "Solution (post-reconstruction into Sygus): " << d_sygus_solution << std::endl; } + }else{ + ////remove boolean ITE (not allowed for sygus comp 2015) + //d_solution = removeBooleanIte( d_solution ); + //Trace("csi-sol") << "Solution (after remove boolean ITE) : " << d_solution << std::endl; } @@ -1278,4 +1420,13 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int& } } +bool CegConjectureSingleInv::needsCheck() { + if( options::cegqiSingleInvMultiInstAbort() ){ + if( !hasITEs() ){ + return d_inst.empty(); + } + } + return true; +} + }
\ No newline at end of file diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h index eb33c479e..f8e3879ac 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.h +++ b/src/theory/quantifiers/ce_guided_single_inv.h @@ -111,8 +111,11 @@ private: bool processSingleInvLiteral( Node lit, bool pol, std::map< Node, std::vector< Node > >& case_vals ); bool doVariableElimination( Node v, std::vector< Node >& conjuncts ); bool getVariableEliminationTerm( bool pol, bool active, Node v, Node n, TNode& s, int& status ); + //presolve + void collectPresolveEqTerms( Node n, std::map< Node, std::vector< Node > >& teq ); + void getPresolveEqConjuncts( std::vector< Node >& vars, std::vector< Node >& terms, std::map< Node, std::vector< Node > >& teq, Node n, std::vector< Node >& conj ); //constructing solution - Node constructSolution( unsigned i, unsigned index ); + Node constructSolution( std::vector< unsigned >& indices, unsigned i, unsigned index ); private: //map from programs to variables in single invocation property std::map< Node, Node > d_single_inv_map; @@ -127,8 +130,6 @@ private: //list of skolems for each program std::vector< Node > d_single_inv_var; //lemmas produced - std::vector< Node > d_lemmas_produced; - std::vector< std::vector< Node > > d_inst; inst::InstMatchTrie d_inst_match_trie; inst::CDInstMatchTrie * d_c_inst_match_trie; // solution @@ -136,6 +137,11 @@ private: Node d_orig_solution; Node d_solution; Node d_sygus_solution; + bool d_has_ites; +public: + //lemmas produced + std::vector< Node > d_lemmas_produced; + std::vector< std::vector< Node > > d_inst; private: std::vector< Node > d_curr_lemmas; //add instantiation @@ -159,8 +165,12 @@ public: void check( std::vector< Node >& lems ); //get solution Node getSolution( unsigned sol_index, TypeNode stn, int& reconstructed ); + // has ites + bool hasITEs() { return d_has_ites; } // is single invocation bool isSingleInvocation() { return !d_single_inv.isNull(); } + //needs check + bool needsCheck(); }; } diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp index 0429abac9..413fd9ba2 100644 --- a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp @@ -86,8 +86,11 @@ Node CegConjectureSingleInvSol::pullITEs( Node s ) { Trace("csi-sol-debug") << "For " << s << ", can pull " << cond << " -> " << t << " with remainder " << rem << std::endl; t = pullITEs( t ); rem = pullITEs( rem ); + Trace("csi-pull-ite") << "PI: Rewrite : " << s << std::endl; + Node prev = s; s = NodeManager::currentNM()->mkNode( ITE, TermDb::simpleNegate( cond ), t, rem ); - //Trace("csi-debug-sol") << "Now : " << s << std::endl; + Trace("csi-pull-ite") << "PI: Rewrite Now : " << s << std::endl; + Trace("csi-pull-ite") << "(= " << prev << " " << s << ")" << std::endl; success = true; } }while( success ); @@ -99,11 +102,13 @@ Node CegConjectureSingleInvSol::pullITEs( Node s ) { bool CegConjectureSingleInvSol::pullITECondition( Node root, Node n_ite, std::vector< Node >& conj, Node& t, Node& rem, int depth ) { Assert( n_ite.getKind()==ITE ); std::vector< Node > curr_conj; + std::vector< Node > orig_conj; bool isAnd; if( n_ite[0].getKind()==AND || n_ite[0].getKind()==OR ){ isAnd = n_ite[0].getKind()==AND; for( unsigned i=0; i<n_ite[0].getNumChildren(); i++ ){ Node cond = n_ite[0][i]; + orig_conj.push_back( cond ); if( n_ite[0].getKind()==OR ){ cond = TermDb::simpleNegate( cond ); } @@ -112,12 +117,15 @@ bool CegConjectureSingleInvSol::pullITECondition( Node root, Node n_ite, std::ve }else{ Node neg = n_ite[0].negate(); if( std::find( conj.begin(), conj.end(), neg )!=conj.end() ){ + //if negation of condition exists, use it isAnd = false; curr_conj.push_back( neg ); }else{ + //otherwise, use condition isAnd = true; curr_conj.push_back( n_ite[0] ); } + orig_conj.push_back( n_ite[0] ); } // take intersection with current conditions std::vector< Node > new_conj; @@ -162,13 +170,14 @@ bool CegConjectureSingleInvSol::pullITECondition( Node root, Node n_ite, std::ve //make remainder : strip out conditions in conj Assert( !conj.empty() ); std::vector< Node > cond_c; + Assert( orig_conj.size()==curr_conj.size() ); for( unsigned i=0; i<curr_conj.size(); i++ ){ if( std::find( conj.begin(), conj.end(), curr_conj[i] )==conj.end() ){ - cond_c.push_back( curr_conj[i] ); + cond_c.push_back( orig_conj[i] ); } } if( cond_c.empty() ){ - rem = isAnd ? tval : rem; + rem = tval; }else{ Node new_cond = cond_c.size()==1 ? cond_c[0] : NodeManager::currentNM()->mkNode( n_ite[0].getKind(), cond_c ); rem = NodeManager::currentNM()->mkNode( ITE, new_cond, isAnd ? tval : rem, isAnd ? rem : tval ); @@ -437,7 +446,7 @@ Node CegConjectureSingleInvSol::simplifySolutionNode( Node sol, TypeNode stn, st ret = NodeManager::currentNM()->mkNode( ITE, exp_c, ret[1], ret[2] ); } if( !d_qe->getTermDatabaseSygus()->hasKind( stnc[0], ret[0].getKind() ) ){ - Trace("csi-sol") << "Flatten based on " << ret[0] << "." << std::endl; + Trace("csi-simp-debug") << "Flatten based on " << ret[0] << "." << std::endl; ret = flattenITEs( ret, false ); } } @@ -510,7 +519,7 @@ Node CegConjectureSingleInvSol::simplifySolutionNode( Node sol, TypeNode stn, st } if( !new_vars.empty() ){ if( !inc.empty() ){ - Node ret = inc.size()==1 ? sol[0] : NodeManager::currentNM()->mkNode( sol.getKind(), inc ); + Node ret = inc.size()==1 ? inc[0] : NodeManager::currentNM()->mkNode( sol.getKind(), inc ); Trace("csi-simp") << "Base return is : " << ret << std::endl; // apply substitution ret = ret.substitute( new_vars.begin(), new_vars.end(), new_subs.begin(), new_subs.end() ); @@ -848,12 +857,10 @@ int CegConjectureSingleInvSol::collectReconstructNodes( Node t, TypeNode stn, in } }while( !new_t.isNull() ); } + //get decompositions for( unsigned i=0; i<dt.getNumConstructors(); i++ ){ Kind k = d_qe->getTermDatabaseSygus()->getArgKind( stn, i ); - if( k==AND || k==OR ){ - equiv.push_back( NodeManager::currentNM()->mkNode( k, min_t, min_t ) ); - equiv.push_back( NodeManager::currentNM()->mkNode( k, min_t, NodeManager::currentNM()->mkConst( k==AND ) ) ); - } + getEquivalentTerms( k, min_t, equiv ); } //assign ids to terms Trace("csi-rcons-debug") << "Term " << id << " is equivalent to " << equiv.size() << " terms : " << std::endl; @@ -1046,4 +1053,62 @@ void CegConjectureSingleInvSol::setReconstructed( int id, Node n ) { } } +void CegConjectureSingleInvSol::getEquivalentTerms( Kind k, Node n, std::vector< Node >& equiv ) { + if( k==AND || k==OR ){ + equiv.push_back( NodeManager::currentNM()->mkNode( k, n, n ) ); + equiv.push_back( NodeManager::currentNM()->mkNode( k, n, NodeManager::currentNM()->mkConst( k==AND ) ) ); + } + //multiplication for integers + //TODO for bitvectors + Kind mk = ( k==PLUS || k==MINUS ) ? MULT : UNDEFINED_KIND; + if( mk!=UNDEFINED_KIND ){ + if( n.getKind()==mk && n[0].isConst() && n[0].getType().isInteger() ){ + bool success = true; + for( unsigned i=0; i<2; i++ ){ + Node eq; + if( k==PLUS || k==MINUS ){ + Node oth = NodeManager::currentNM()->mkConst( Rational(i==0 ? 1000 : -1000) ); + eq = i==0 ? NodeManager::currentNM()->mkNode( LEQ, n[0], oth ) : NodeManager::currentNM()->mkNode( GEQ, n[0], oth ); + } + if( !eq.isNull() ){ + eq = Rewriter::rewrite( eq ); + if( eq!=d_qe->getTermDatabase()->d_true ){ + success = false; + break; + } + } + } + if( success ){ + Node var = n[1]; + Node rem; + if( k==PLUS || k==MINUS ){ + int rem_coeff = (int)n[0].getConst<Rational>().getNumerator().getSignedInt(); + if( rem_coeff>0 && k==PLUS ){ + rem_coeff--; + }else if( rem_coeff<0 && k==MINUS ){ + rem_coeff++; + }else{ + success = false; + } + if( success ){ + rem = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(rem_coeff) ), var ); + rem = Rewriter::rewrite( rem ); + } + } + if( !rem.isNull() ){ + equiv.push_back( NodeManager::currentNM()->mkNode( k, rem, var ) ); + } + } + } + } + //negative constants + if( k==MINUS ){ + if( n.isConst() && n.getType().isInteger() && n.getConst<Rational>().getNumerator().strictlyNegative() ){ + Node nn = NodeManager::currentNM()->mkNode( UMINUS, n ); + nn = Rewriter::rewrite( nn ); + equiv.push_back( NodeManager::currentNM()->mkNode( MINUS, NodeManager::currentNM()->mkConst( Rational(0) ), nn ) ); + } + } +} + } diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.h b/src/theory/quantifiers/ce_guided_single_inv_sol.h index 6a4b6f90f..1d84986b4 100644 --- a/src/theory/quantifiers/ce_guided_single_inv_sol.h +++ b/src/theory/quantifiers/ce_guided_single_inv_sol.h @@ -78,6 +78,8 @@ private: bool collectReconstructNodes( int pid, std::vector< Node >& ts, const DatatypeConstructor& dtc, std::vector< int >& ids, int& status ); bool getPathToRoot( int id ); void setReconstructed( int id, Node n ); + //get equivalent terms to n with top symbol k + void getEquivalentTerms( Kind k, Node n, std::vector< Node >& equiv ); public: Node reconstructSolution( Node sol, TypeNode stn, int& reconstructed ); public: diff --git a/src/theory/quantifiers/fun_def_engine.cpp b/src/theory/quantifiers/fun_def_engine.cpp new file mode 100644 index 000000000..56214f540 --- /dev/null +++ b/src/theory/quantifiers/fun_def_engine.cpp @@ -0,0 +1,54 @@ +/********************* */ +/*! \file fun_def_process.cpp + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** This class implements specialized techniques for (recursively) defined functions + **/ + +#include <vector> + +#include "theory/quantifiers/fun_def_engine.h" +#include "theory/rewriter.h" +#include "theory/quantifiers/term_database.h" + +using namespace CVC4; +using namespace std; +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; +using namespace CVC4::kind; + +FunDefEngine::FunDefEngine( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ) { + +} + +/* whether this module needs to check this round */ +bool FunDefEngine::needsCheck( Theory::Effort e ) { + return e>=Theory::EFFORT_LAST_CALL; +} + +/* reset at a round */ +void FunDefEngine::reset_round( Theory::Effort e ){ + //TODO +} + +/* Call during quantifier engine's check */ +void FunDefEngine::check( Theory::Effort e, unsigned quant_e ) { + //TODO +} + +/* Called for new quantifiers */ +void FunDefEngine::registerQuantifier( Node q ) { + //TODO +} + +/** called for everything that gets asserted */ +void FunDefEngine::assertNode( Node n ) { + //TODO +} diff --git a/src/theory/quantifiers/fun_def_engine.h b/src/theory/quantifiers/fun_def_engine.h new file mode 100644 index 000000000..be73d51a9 --- /dev/null +++ b/src/theory/quantifiers/fun_def_engine.h @@ -0,0 +1,59 @@ +/********************* */ +/*! \file fun_def_engine.h + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Specialized techniques for (recursively) defined functions + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__QUANTIFIERS_FUN_DEF_ENGINE_H +#define __CVC4__QUANTIFIERS_FUN_DEF_ENGINE_H + +#include <iostream> +#include <string> +#include <vector> +#include <map> +#include "expr/node.h" +#include "expr/type_node.h" +#include "theory/quantifiers_engine.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +//module for handling (recursively) defined functions +class FunDefEngine : public QuantifiersModule { +private: + +public: + FunDefEngine( QuantifiersEngine * qe, context::Context* c ); + ~FunDefEngine(){} + + /* whether this module needs to check this round */ + bool needsCheck( Theory::Effort e ); + /* reset at a round */ + void reset_round( Theory::Effort e ); + /* Call during quantifier engine's check */ + void check( Theory::Effort e, unsigned quant_e ); + /* Called for new quantifiers */ + void registerQuantifier( Node q ); + /** called for everything that gets asserted */ + void assertNode( Node n ); + /** Identify this module (for debugging, dynamic configuration, etc..) */ + std::string identify() const { return "FunDefEngine"; } +}; + + +} +} +} + +#endif diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 391abe9eb..ab0526471 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -220,8 +220,12 @@ option cegqiSingleInvReconstruct --cegqi-si-reconstruct bool :default true reconstruct solutions for single invocation conjectures in original grammar option cegqiSingleInvReconstructConst --cegqi-si-reconstruct-const bool :default true include constants when reconstruct solutions for single invocation conjectures in original grammar +option cegqiSingleInvPreRegInst --cegqi-si-prereg-inst bool :default true + preregister ground instantiations when single invocation option cegqiSingleInvAbort --cegqi-si-abort bool :default false - abort if our synthesis conjecture is not single invocation + 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 @@ -259,5 +263,10 @@ option lteRestrictInstClosure --lte-restrict-inst-closure bool :default false option quantAlphaEquiv --quant-alpha-equiv bool :default true infer alpha equivalence between quantified formulas + +### recursive function options + +#option funDefs --fun-defs bool :default false +# enable specialized techniques for recursive function definitions endmodule diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 0198e014f..6a95e243d 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -905,7 +905,21 @@ Node QuantifiersRewriter::computeSplit( Node f, Node body, std::vector< Node >& Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, Node ipl ){ std::vector< Node > activeArgs; - computeArgVec2( args, activeArgs, body, ipl ); + //if cegqi is on, may be synthesis conjecture, in which case we want to keep all variables + if( options::ceGuidedInst() && !ipl.isNull() ){ + for( unsigned i=0; i<ipl.getNumChildren(); i++ ){ + Trace("quant-attr-debug") << "Check : " << ipl[i] << " " << ipl[i].getKind() << std::endl; + if( ipl[i].getKind()==INST_ATTRIBUTE ){ + Node avar = ipl[i][0]; + if( avar.getAttribute(SygusAttribute()) ){ + activeArgs.insert( activeArgs.end(), args.begin(), args.end() ); + } + } + } + } + if( activeArgs.empty() ){ + computeArgVec2( args, activeArgs, body, ipl ); + } if( activeArgs.empty() ){ return body; }else{ diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index cc8ae4db0..fa0e211b3 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -23,6 +23,7 @@ #include "theory/datatypes/datatypes_rewriter.h" #include "theory/quantifiers/ce_guided_instantiation.h" #include "theory/quantifiers/rewrite_engine.h" +#include "theory/quantifiers/fun_def_engine.h" //for sygus #include "theory/bv/theory_bv_utils.h" @@ -1431,6 +1432,7 @@ void TermDb::computeAttributes( Node q ) { exit( 0 ); } d_fun_defs[f] = true; + d_quantEngine->setOwner( q, d_quantEngine->getFunDefEngine() ); } if( avar.getAttribute(SygusAttribute()) ){ //not necessarily nested existential @@ -1578,7 +1580,7 @@ TNode TermDbSygus::getVarInc( TypeNode tn, std::map< TypeNode, int >& var_count } } -TypeNode TermDbSygus::getSygusType( Node v ) { +TypeNode TermDbSygus::getSygusTypeForVar( Node v ) { Assert( d_fv_stype.find( v )!=d_fv_stype.end() ); return d_fv_stype[v]; } @@ -1740,7 +1742,7 @@ Node TermDbSygus::mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int Node n = NodeManager::currentNM()->mkNode( APPLY, children ); //must expand definitions Node ne = Node::fromExpr( smt::currentSmtEngine()->expandDefinitions( n.toExpr() ) ); - Trace("sygus-util-debug") << "Expanded definitions in " << n << " to " << ne << std::endl; + Trace("sygus-db-debug") << "Expanded definitions in " << n << " to " << ne << std::endl; return ne; */ } @@ -2093,10 +2095,10 @@ void TermDbSygus::registerSygusType( TypeNode tn ){ d_register[tn] = TypeNode::null(); }else{ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - Trace("sygus-util") << "Register type " << dt.getName() << "..." << std::endl; + Trace("sygus-db") << "Register type " << dt.getName() << "..." << std::endl; d_register[tn] = TypeNode::fromType( dt.getSygusType() ); if( d_register[tn].isNull() ){ - Trace("sygus-util") << "...not sygus." << std::endl; + Trace("sygus-db") << "...not sygus." << std::endl; }else{ //for constant reconstruction Kind ck = getComparisonKind( TypeNode::fromType( dt.getSygusType() ) ); @@ -2107,14 +2109,14 @@ void TermDbSygus::registerSygusType( TypeNode tn ){ Expr sop = dt[i].getSygusOp(); Assert( !sop.isNull() ); Node n = Node::fromExpr( sop ); - Trace("sygus-util") << " Operator #" << i << " : " << sop; + Trace("sygus-db") << " Operator #" << i << " : " << sop; if( sop.getKind() == kind::BUILTIN ){ Kind sk = NodeManager::operatorToKind( n ); - Trace("sygus-util") << ", kind = " << sk; + Trace("sygus-db") << ", kind = " << sk; d_kinds[tn][sk] = i; d_arg_kind[tn][i] = sk; }else if( sop.isConst() ){ - Trace("sygus-util") << ", constant"; + Trace("sygus-db") << ", constant"; d_consts[tn][n] = i; d_arg_const[tn][i] = n; d_const_list[tn].push_back( n ); @@ -2127,7 +2129,7 @@ void TermDbSygus::registerSygusType( TypeNode tn ){ } d_ops[tn][n] = i; d_arg_ops[tn][i] = n; - Trace("sygus-util") << std::endl; + Trace("sygus-db") << std::endl; } //sort the constant list if( !d_const_list[tn].empty() ){ @@ -2137,12 +2139,12 @@ void TermDbSygus::registerSygusType( TypeNode tn ){ sc.d_tds = this; std::sort( d_const_list[tn].begin(), d_const_list[tn].end(), sc ); } - Trace("sygus-util") << "Type has " << d_const_list[tn].size() << " constants..." << std::endl << " "; + Trace("sygus-db") << "Type has " << d_const_list[tn].size() << " constants..." << std::endl << " "; for( unsigned i=0; i<d_const_list[tn].size(); i++ ){ - Trace("sygus-util") << d_const_list[tn][i] << " "; + Trace("sygus-db") << d_const_list[tn][i] << " "; } - Trace("sygus-util") << std::endl; - Trace("sygus-util") << "Of these, " << d_const_list_pos[tn] << " are marked as positive." << std::endl; + Trace("sygus-db") << std::endl; + Trace("sygus-db") << "Of these, " << d_const_list_pos[tn] << " are marked as positive." << std::endl; } //register connected types for( unsigned i=0; i<dt.getNumConstructors(); i++ ){ @@ -2159,6 +2161,11 @@ bool TermDbSygus::isRegistered( TypeNode tn ) { return d_register.find( tn )!=d_register.end(); } +TypeNode TermDbSygus::sygusToBuiltinType( TypeNode tn ) { + Assert( isRegistered( tn ) ); + return d_register[tn]; +} + int TermDbSygus::getKindArg( TypeNode tn, Kind k ) { Assert( isRegistered( tn ) ); std::map< TypeNode, std::map< Kind, int > >::iterator itt = d_kinds.find( tn ); @@ -2348,6 +2355,7 @@ bool TermDbSygus::doCompare( Node a, Node b, Kind k ) { return com==d_true; } + void doStrReplace(std::string& str, const std::string& oldStr, const std::string& newStr){ size_t pos = 0; while((pos = str.find(oldStr, pos)) != std::string::npos){ @@ -2367,7 +2375,20 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node > if( n.getNumChildren()>0 ){ out << "("; } - out << dt[cIndex].getSygusOp(); + Node op = dt[cIndex].getSygusOp(); + if( op.getType().isBitVector() && op.isConst() ){ + //print in the style it was given + Trace("sygus-print-bvc") << "[Print " << op << " " << dt[cIndex].getName() << "]" << std::endl; + std::stringstream ss; + ss << dt[cIndex].getName(); + std::string str = ss.str(); + std::size_t found = str.find_last_of("_"); + Assert( found!=std::string::npos ); + std::string name = std::string( str.begin() + found +1, str.end() ); + out << name; + }else{ + out << op; + } if( n.getNumChildren()>0 ){ for( unsigned i=0; i<n.getNumChildren(); i++ ){ out << " "; @@ -2376,9 +2397,10 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node > out << ")"; } }else{ + std::stringstream let_out; //print as let term if( dt[cIndex].getNumSygusLetInputArgs()>0 ){ - out << "(let ("; + let_out << "(let ("; } std::vector< Node > subs_lvs; std::vector< Node > new_lvs; @@ -2392,22 +2414,25 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node > //map free variables to proper terms if( i<dt[cIndex].getNumSygusLetInputArgs() ){ //it should be printed as a let argument - out << "("; - out << lv << " " << lv.getType() << " "; - printSygusTerm( out, n[i], lvs ); - out << ")"; + let_out << "("; + let_out << lv << " " << lv.getType() << " "; + printSygusTerm( let_out, n[i], lvs ); + let_out << ")"; } } if( dt[cIndex].getNumSygusLetInputArgs()>0 ){ - out << ") "; + let_out << ") "; } //print the body Node let_body = Node::fromExpr( dt[cIndex].getSygusLetBody() ); let_body = let_body.substitute( subs_lvs.begin(), subs_lvs.end(), new_lvs.begin(), new_lvs.end() ); new_lvs.insert( new_lvs.end(), lvs.begin(), lvs.end() ); - std::stringstream body_out; - printSygusTerm( body_out, let_body, new_lvs ); - std::string body = body_out.str(); + printSygusTerm( let_out, let_body, new_lvs ); + if( dt[cIndex].getNumSygusLetInputArgs()>0 ){ + let_out << ")"; + } + //do variable substitutions since ASSUMING : let_vars are interpreted literally and do not represent a class of variables + std::string lbody = let_out.str(); for( unsigned i=0; i<dt[cIndex].getNumSygusLetArgs(); i++ ){ std::stringstream old_str; old_str << new_lvs[i]; @@ -2417,12 +2442,9 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node > }else{ new_str << Node::fromExpr( dt[cIndex].getSygusLetArg( i ) ); } - doStrReplace( body, old_str.str().c_str(), new_str.str().c_str() ); - } - out << body; - if( dt[cIndex].getNumSygusLetInputArgs()>0 ){ - out << ")"; + doStrReplace( lbody, old_str.str().c_str(), new_str.str().c_str() ); } + out << lbody; } return; } diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index e61552713..1ffe0e29e 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -433,7 +433,7 @@ public: bool getMatch( Node n, TypeNode st, int& index_found, std::vector< Node >& args, int index_exc = -1, int index_start = 0 ); private: //information for sygus types - std::map< TypeNode, TypeNode > d_register; //stores sygus type + std::map< TypeNode, TypeNode > d_register; //stores sygus -> builtin type std::map< TypeNode, std::map< int, Kind > > d_arg_kind; std::map< TypeNode, std::map< Kind, int > > d_kinds; std::map< TypeNode, std::map< int, Node > > d_arg_const; @@ -455,6 +455,7 @@ private: public: TermDbSygus(); bool isRegistered( TypeNode tn ); + TypeNode sygusToBuiltinType( TypeNode tn ); int getKindArg( TypeNode tn, Kind k ); int getConstArg( TypeNode tn, Node n ); int getOpArg( TypeNode tn, Node n ); @@ -485,7 +486,7 @@ public: Node getTypeValueOffset( TypeNode tn, Node val, int offset, int& status ); /** get value */ Node getTypeMaxValue( TypeNode tn ); - TypeNode getSygusType( Node v ); + TypeNode getSygusTypeForVar( Node v ); Node mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int >& var_count, std::map< int, Node >& pre ); Node sygusToBuiltin( Node n, TypeNode tn ); Node builtinToSygusConst( Node c, TypeNode tn, int rcons_depth = 0 ); diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 9f8f0d6cf..ccbbd5bd5 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -37,6 +37,7 @@ #include "theory/uf/theory_uf.h" #include "theory/quantifiers/full_model_check.h" #include "theory/quantifiers/ambqi_builder.h" +#include "theory/quantifiers/fun_def_engine.h" using namespace std; using namespace CVC4; @@ -169,6 +170,12 @@ d_lemmas_produced_c(u){ }else{ d_alpha_equiv = NULL; } + //if( options::funDefs() ){ + // d_fun_def_engine = new quantifiers::FunDefEngine( this, c ); + // d_modules.push_back( d_fun_def_engine ); + //}else{ + d_fun_def_engine = NULL; + //} if( needsBuilder ){ Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBoundInt() << std::endl; @@ -208,6 +215,7 @@ QuantifiersEngine::~QuantifiersEngine(){ delete d_sg_gen; delete d_ceg_inst; delete d_lte_part_inst; + delete d_fun_def_engine; for(std::map< Node, QuantPhaseReq* >::iterator i = d_phase_reqs.begin(); i != d_phase_reqs.end(); ++i) { delete (*i).second; } diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 3040a35c7..54f63bfe0 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -93,6 +93,7 @@ namespace quantifiers { class CegInstantiation; class LtePartialInst; class AlphaEquivalence; + class FunDefEngine; }/* CVC4::theory::quantifiers */ namespace inst { @@ -142,6 +143,8 @@ private: quantifiers::CegInstantiation * d_ceg_inst; /** lte partial instantiation */ quantifiers::LtePartialInst * d_lte_part_inst; + /** function definitions engine */ + quantifiers::FunDefEngine * d_fun_def_engine; public: //effort levels enum { QEFFORT_CONFLICT, @@ -228,6 +231,8 @@ public: //modules quantifiers::CegInstantiation * getCegInstantiation() { return d_ceg_inst; } /** local theory ext partial inst */ quantifiers::LtePartialInst * getLtePartialInst() { return d_lte_part_inst; } + /** function definition engine */ + quantifiers::FunDefEngine * getFunDefEngine() { return d_fun_def_engine; } private: /** owner of quantified formulas */ std::map< Node, QuantifiersModule * > d_owner; |