diff options
author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2015-07-27 20:19:35 -0500 |
---|---|---|
committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2015-07-27 20:19:35 -0500 |
commit | 8f4a7df9bd9cb59826e9769802d1345877a392ef (patch) | |
tree | e0797f3a9a4160c6199ecfd5deb7727e562a5e91 /src/theory | |
parent | 9f10a95e26e9e790a19a6f9e68a658ec2ab6d304 (diff) | |
parent | c0079b3110a81f2ff993b7f86782266380dd102e (diff) |
Merge branch 'master' of https://github.com/CVC4/CVC4
Diffstat (limited to 'src/theory')
47 files changed, 1894 insertions, 744 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 d08c92dd9..3ab29f334 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -88,7 +88,7 @@ void SygusSplit::getSygusSplits( Node n, const Datatype& dt, std::vector< Node > Kind k = d_tds->getArgKind( tnnp, csIndex ); //size comparison for arguments (if necessary) Node sz_leq; - if( tn1==tnn && d_tds->isComm( k ) ){ + if( tn1==tnn && quantifiers::TermDb::isComm( k ) ){ sz_leq = NodeManager::currentNM()->mkNode( LEQ, NodeManager::currentNM()->mkNode( DT_SIZE, n ), NodeManager::currentNM()->mkNode( DT_SIZE, arg1 ) ); } std::map< int, std::vector< int > >::iterator it = d_sygus_pc_arg_pos[tnn][csIndex].find( i ); @@ -327,7 +327,7 @@ void SygusSplit::registerSygusTypeConstructorArg( TypeNode tnn, const Datatype& Assert( d_sygus_pc_nred[tnn][csIndex].find( sIndex )!=d_sygus_pc_nred[tnn][csIndex].end() ); Assert( d_sygus_pc_nred[tnno][csIndex].find( osIndex )!=d_sygus_pc_nred[tnno][csIndex].end() ); - bool isPComm = d_tds->isComm( parentKind ); + bool isPComm = quantifiers::TermDb::isComm( parentKind ); std::map< int, bool > larg_consider; for( unsigned i=0; i<dto.getNumConstructors(); i++ ){ if( d_sygus_pc_nred[tnno][csIndex][osIndex][i] ){ @@ -411,7 +411,7 @@ bool SygusSplit::considerSygusSplitKind( const Datatype& dt, const Datatype& pdt int pc = d_tds->getKindArg( tnp, parent ); if( k==parent ){ //check for associativity - if( d_tds->isAssoc( k ) ){ + if( quantifiers::TermDb::isAssoc( k ) ){ //if the operator is associative, then a repeated occurrence should only occur in the leftmost argument position int firstArg = getFirstArgOccurrence( pdt[pc], dt ); Assert( firstArg!=-1 ); @@ -511,8 +511,8 @@ bool SygusSplit::considerSygusSplitKind( const Datatype& dt, const Datatype& pdt } } if( parent==MINUS || parent==BITVECTOR_SUB ){ - - + + } return true; } @@ -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; @@ -820,10 +830,10 @@ bool SygusSymBreak::processCurrentProgram( Node a, TypeNode at, int depth, Node Node progr = d_tds->getNormalized( at, prog ); Node rep_prog; std::map< Node, Node >::iterator itnp = d_normalized_to_orig[at].find( progr ); - int tsize = d_tds->getTermSize( prog ); + 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/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp new file mode 100755 index 000000000..e4dcccdff --- /dev/null +++ b/src/theory/quantifiers/alpha_equivalence.cpp @@ -0,0 +1,105 @@ +/********************* */ +/*! \file alpha_equivalence.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-2015 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Alpha equivalence checking + ** + **/ + +#include "theory/quantifiers/alpha_equivalence.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; + +struct sortTypeOrder { + TermDb* d_tdb; + bool operator() (TypeNode i, TypeNode j) { + return d_tdb->getIdForType( i )<d_tdb->getIdForType( j ); + } +}; + +bool AlphaEquivalenceNode::registerNode( QuantifiersEngine* qe, Node q, std::vector< Node >& tt, std::vector< int >& arg_index ) { + if( tt.size()==arg_index.size()+1 ){ + Node t = tt.back(); + Node op = t.hasOperator() ? t.getOperator() : t; + arg_index.push_back( 0 ); + Trace("aeq-debug") << op << " "; + return d_children[op][t.getNumChildren()].registerNode( qe, q, tt, arg_index ); + }else if( tt.empty() ){ + //we are finished + Trace("aeq-debug") << std::endl; + if( d_quant.isNull() ){ + d_quant = q; + return true; + }else{ + //lemma ( q <=> d_quant ) + Trace("alpha-eq") << "Alpha equivalent : " << std::endl; + Trace("alpha-eq") << " " << q << std::endl; + Trace("alpha-eq") << " " << d_quant << std::endl; + qe->getOutputChannel().lemma( q.iffNode( d_quant ) ); + return false; + } + }else{ + Node t = tt.back(); + int i = arg_index.back(); + if( i==(int)t.getNumChildren() ){ + tt.pop_back(); + arg_index.pop_back(); + }else{ + tt.push_back( t[i] ); + arg_index[arg_index.size()-1]++; + } + return registerNode( qe, q, tt, arg_index ); + } +} + +bool AlphaEquivalenceTypeNode::registerNode( QuantifiersEngine* qe, Node q, Node t, std::vector< TypeNode >& typs, std::map< TypeNode, int >& typ_count, int index ){ + if( index==(int)typs.size() ){ + std::vector< Node > tt; + std::vector< int > arg_index; + tt.push_back( t ); + Trace("aeq-debug") << " : "; + return d_data.registerNode( qe, q, tt, arg_index ); + }else{ + TypeNode curr = typs[index]; + Assert( typ_count.find( curr )!=typ_count.end() ); + Trace("aeq-debug") << "[" << curr << " " << typ_count[curr] << "] "; + return d_children[curr][typ_count[curr]].registerNode( qe, q, t, typs, typ_count, index+1 ); + } +} + +bool AlphaEquivalence::registerQuantifier( Node q ) { + Assert( q.getKind()==FORALL ); + Trace("aeq") << "Alpha equivalence : register " << q << std::endl; + //construct canonical quantified formula + Node t = d_qe->getTermDatabase()->getCanonicalTerm( q[1], true ); + Trace("aeq") << " canonical form: " << t << std::endl; + //compute variable type counts + std::map< TypeNode, int > typ_count; + std::vector< TypeNode > typs; + for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ + TypeNode tn = q[0][i].getType(); + typ_count[tn]++; + if( std::find( typs.begin(), typs.end(), tn )==typs.end() ){ + typs.push_back( tn ); + } + } + sortTypeOrder sto; + sto.d_tdb = d_qe->getTermDatabase(); + std::sort( typs.begin(), typs.end(), sto ); + Trace("aeq-debug") << " "; + bool ret = d_ae_typ_trie.registerNode( d_qe, q, t, typs, typ_count ); + Trace("aeq") << " ...result : " << ret << std::endl; + return ret; +} diff --git a/src/theory/quantifiers/alpha_equivalence.h b/src/theory/quantifiers/alpha_equivalence.h new file mode 100755 index 000000000..fa2109ccc --- /dev/null +++ b/src/theory/quantifiers/alpha_equivalence.h @@ -0,0 +1,57 @@ +/********************* */ +/*! \file alpha_equivalence.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-2015 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Alpha equivalence checking + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__ALPHA_EQUIVALENCE_H +#define __CVC4__ALPHA_EQUIVALENCE_H + + +#include "theory/quantifiers_engine.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +class AlphaEquivalenceNode { +public: + std::map< Node, std::map< int, AlphaEquivalenceNode > > d_children; + Node d_quant; + bool registerNode( QuantifiersEngine* qe, Node q, std::vector< Node >& tt, std::vector< int >& arg_index ); +}; + +class AlphaEquivalenceTypeNode { +public: + std::map< TypeNode, std::map< int, AlphaEquivalenceTypeNode > > d_children; + AlphaEquivalenceNode d_data; + bool registerNode( QuantifiersEngine* qe, Node q, Node t, std::vector< TypeNode >& typs, std::map< TypeNode, int >& typ_count, int index = 0 ); +}; + +class AlphaEquivalence { +private: + QuantifiersEngine* d_qe; + //per # of variables per type + AlphaEquivalenceTypeNode d_ae_typ_trie; +public: + AlphaEquivalence( QuantifiersEngine* qe ) : d_qe( qe ){} + ~AlphaEquivalence(){} + + bool registerQuantifier( Node q ); +}; + +} +} +} + +#endif diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index 5f3498f49..e10ba0fef 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -37,14 +37,25 @@ CegConjecture::CegConjecture( context::Context* c ) : d_active( c, false ), d_in void CegConjecture::assign( QuantifiersEngine * qe, Node q ) { Assert( d_quant.isNull() ); Assert( q.getKind()==FORALL ); + d_assert_quant = q; + //register with single invocation if applicable + if( qe->getTermDatabase()->isQAttrSygus( d_assert_quant ) && options::cegqiSingleInv() ){ + d_ceg_si->initialize( qe, q ); + if( q!=d_ceg_si->d_quant ){ + //Node red_lem = NodeManager::currentNM()->mkNode( OR, q.negate(), d_cegqi_si->d_quant ); + //may have rewritten quantified formula (for invariant synthesis) + q = d_ceg_si->d_quant; + } + } d_quant = q; for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ d_candidates.push_back( NodeManager::currentNM()->mkSkolem( "e", q[0][i].getType() ) ); } + Trace("cegqi") << "Base quantified fm is : " << q << std::endl; //construct base instantiation d_base_inst = Rewriter::rewrite( qe->getInstantiation( q, d_candidates ) ); Trace("cegqi") << "Base instantiation is : " << d_base_inst << std::endl; - if( qe->getTermDatabase()->isQAttrSygus( q ) ){ + if( qe->getTermDatabase()->isQAttrSygus( d_assert_quant ) ){ CegInstantiation::collectDisjuncts( d_base_inst, d_base_disj ); Trace("cegqi") << "Conjecture has " << d_base_disj.size() << " disjuncts." << std::endl; //store the inner variables for each disjunct @@ -59,10 +70,7 @@ void CegConjecture::assign( QuantifiersEngine * qe, Node q ) { } } d_syntax_guided = true; - if( options::cegqiSingleInv() ){ - d_ceg_si->initialize( qe, q ); - } - }else if( qe->getTermDatabase()->isQAttrSynthesis( q ) ){ + }else if( qe->getTermDatabase()->isQAttrSynthesis( d_assert_quant ) ){ d_syntax_guided = false; }else{ Assert( false ); @@ -70,7 +78,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 +145,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 +167,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; @@ -207,35 +219,38 @@ void CegInstantiation::assertNode( Node n ) { //d_guard_assertions[lit] = pol; d_conj->d_infeasible = !pol; } - if( lit==d_conj->d_quant ){ + if( lit==d_conj->d_assert_quant ){ d_conj->d_active = true; } } 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; } } @@ -244,6 +259,7 @@ Node CegInstantiation::getNextDecisionRequest() { void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { Node q = conj->d_quant; + Node aq = conj->d_assert_quant; Trace("cegqi-engine-debug") << "Synthesis conjecture : " << q << std::endl; Trace("cegqi-engine-debug") << " * Candidate program/output symbol : "; for( unsigned i=0; i<conj->d_candidates.size(); i++ ){ @@ -256,7 +272,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { if( conj->d_ce_sk.empty() ){ Trace("cegqi-engine") << " *** Check candidate phase..." << std::endl; - if( getTermDatabase()->isQAttrSygus( q ) ){ + if( conj->d_syntax_guided ){ if( conj->d_ceg_si ){ std::vector< Node > lems; conj->d_ceg_si->check( lems ); @@ -296,7 +312,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { conj->d_ce_sk.push_back( std::vector< Node >() ); } std::vector< Node > ic; - ic.push_back( q.negate() ); + ic.push_back( aq.negate() ); std::vector< Node > d; collectDisjuncts( inst, d ); Assert( d.size()==conj->d_base_disj.size() ); @@ -327,7 +343,8 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { Trace("cegqi-engine") << " ...find counterexample." << std::endl; } - }else if( getTermDatabase()->isQAttrSynthesis( q ) ){ + }else{ + Assert( aq==q ); std::vector< Node > model_terms; if( getModelValues( conj, conj->d_candidates, model_terms ) ){ d_quantEngine->addInstantiation( q, model_terms, false ); @@ -484,16 +501,18 @@ 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; //} for( unsigned i=0; i<d_conj->d_candidates.size(); i++ ){ + Node prog = d_conj->d_quant[0][i]; std::stringstream ss; - ss << d_conj->d_quant[0][i]; + ss << prog; std::string f(ss.str()); f.erase(f.begin()); - TypeNode tn = d_conj->d_quant[0][i].getType(); + TypeNode tn = prog.getType(); Assert( datatypes::DatatypesRewriter::isTypeDatatype( tn ) ); const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); Assert( dt.isSygus() ); @@ -506,7 +525,34 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) { }else{ if( !d_conj->d_candidate_inst[i].empty() ){ sol = d_conj->d_candidate_inst[i].back(); - status = 1; + //check if this was based on a template, if so, we must do reconstruction + if( d_conj->d_assert_quant!=d_conj->d_quant ){ + Trace("cegqi-inv") << "Sygus version of solution is : " << sol << ", type : " << sol.getType() << std::endl; + sol = getTermDatabase()->getTermDatabaseSygus()->sygusToBuiltin( sol, sol.getType() ); + Trace("cegqi-inv") << "Builtin version of solution is : " << sol << ", type : " << sol.getType() << std::endl; + std::vector< Node > subs; + Expr svl = dt.getSygusVarList(); + for( unsigned j=0; j<svl.getNumChildren(); j++ ){ + subs.push_back( Node::fromExpr( svl[j] ) ); + } + if( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_PRE ){ + Node pre = d_conj->d_ceg_si->d_trans_pre[prog]; + pre = pre.substitute( d_conj->d_ceg_si->d_prog_templ_vars[prog].begin(), d_conj->d_ceg_si->d_prog_templ_vars[prog].end(), + subs.begin(), subs.end() ); + sol = NodeManager::currentNM()->mkNode( OR, sol, pre ); + }else if( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_POST ){ + Node post = d_conj->d_ceg_si->d_trans_post[prog]; + post = post.substitute( d_conj->d_ceg_si->d_prog_templ_vars[prog].begin(), d_conj->d_ceg_si->d_prog_templ_vars[prog].end(), + subs.begin(), subs.end() ); + sol = NodeManager::currentNM()->mkNode( AND, sol, post ); + } + Trace("cegqi-inv-debug") << "With template : " << sol << std::endl; + sol = Rewriter::rewrite( sol ); + Trace("cegqi-inv-debug") << "Simplified : " << sol << std::endl; + sol = d_conj->d_ceg_si->reconstructToSyntax( sol, tn, status ); + }else{ + status = 1; + } } } if( !(Trace.isOn("cegqi-stats")) ){ @@ -530,6 +576,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..af3a19d62 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.h +++ b/src/theory/quantifiers/ce_guided_instantiation.h @@ -35,7 +35,9 @@ public: context::CDO< bool > d_active; /** is conjecture infeasible */ context::CDO< bool > d_infeasible; - /** quantified formula */ + /** quantified formula asserted */ + Node d_assert_quant; + /** quantified formula (after processing) */ Node d_quant; /** guard */ Node d_guard; @@ -83,6 +85,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 22ffcd278..ef2e3005e 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -538,6 +538,7 @@ bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< d_qe->getOutputChannel().lemma( delta_lem ); } subs[i] = NodeManager::currentNM()->mkNode( subs_typ[i]==2 ? PLUS : MINUS, subs[i], d_n_delta ); + d_used_delta = true; } } //check if we have already added this instantiation @@ -706,7 +707,7 @@ void CegInstantiator::getDeltaLemmas( std::vector< Node >& lems ) { */ } -void CegInstantiator::check() { +bool CegInstantiator::check() { for( unsigned r=0; r<2; r++ ){ std::vector< Node > subs; @@ -716,10 +717,11 @@ void CegInstantiator::check() { std::vector< int > subs_typ; //try to add an instantiation if( addInstantiation( subs, vars, coeff, has_coeff, subs_typ, 0, r==0 ? 0 : 2 ) ){ - return; + return true; } } Trace("cegqi-engine") << " WARNING : unable to find CEGQI single invocation instantiation." << std::endl; + return false; } @@ -740,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{ @@ -788,9 +799,18 @@ 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; + bool invExtractPrePost = false; if( analyzeSygusConjunct( Node::null(), q[1], children, prog_invoke, progs, contains, true ) ){ singleInvocation = true; //try to phrase as single invocation property @@ -807,7 +827,6 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) { for( std::map< Node, std::vector< Node > >::iterator it2 = itp->second.begin(); it2 != itp->second.end(); ++it2 ){ if( it2->second.size()>1 ){ singleInvocation = false; - break; }else if( it2->second.size()==1 ){ Node prog = it2->first; Node inv = it2->second[0]; @@ -821,15 +840,26 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) { single_invoke_args[prog][k-1].push_back( arg ); } } + if( inv.getType().isBoolean() ){ + //conjunct defines pre and/or post conditions + if( options::sygusInvTemplMode() != SYGUS_INV_TEMPL_MODE_NONE ){ + invExtractPrePost = true; + } + } } } } } } - if( singleInvocation ){ + if( singleInvocation || invExtractPrePost ){ + //no value in extracting pre/post if we are single invocation + if( singleInvocation ){ + invExtractPrePost = false; + } Trace("cegqi-si") << "Property is single invocation with : " << std::endl; std::vector< Node > pbvs; std::vector< Node > new_vars; + std::map< Node, std::vector< Node > > prog_vars; std::map< Node, std::vector< Node > > new_assumptions; for( std::map< Node, std::vector< Node > >::iterator it = invocations.begin(); it != invocations.end(); ++it ){ Assert( !it->second.empty() ); @@ -849,12 +879,14 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) { Assert( !single_invoke_args[prog][k-1].empty() ); if( single_invoke_args[prog][k-1].size()==1 && single_invoke_args[prog][k-1][0].getKind()==BOUND_VARIABLE ){ invc.push_back( single_invoke_args[prog][k-1][0] ); + prog_vars[prog].push_back( single_invoke_args[prog][k-1][0] ); }else{ //introduce fresh variable, assign all Node v = NodeManager::currentNM()->mkSkolem( "a", single_invoke_args[prog][k-1][0].getType(), "single invocation arg" ); new_vars.push_back( v ); invc.push_back( v ); d_single_inv_arg_sk.push_back( v ); + prog_vars[prog].push_back( v ); for( unsigned i=0; i<single_invoke_args[prog][k-1].size(); i++ ){ Node arg = single_invoke_args[prog][k-1][i]; @@ -878,13 +910,16 @@ 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() ); std::vector< Node > conjuncts; + std::vector< Node > conjuncts_si_progs; + std::vector< Node > conjuncts_si_invokes; for( unsigned i=0; i<it->second.size(); i++ ){ Node c = it->second[i]; std::vector< Node > disj; @@ -896,17 +931,32 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) { if( itp!=prog_invoke.end() ){ std::vector< Node > terms; std::vector< Node > subs; + std::vector< Node > progs; for( std::map< Node, std::vector< Node > >::iterator it2 = itp->second.begin(); it2 != itp->second.end(); ++it2 ){ - if( !it2->second.empty() ){ + if( it2->second.size()==1 ){ Node prog = it2->first; Node inv = it2->second[0]; Assert( it2->second.size()==1 ); terms.push_back( inv ); subs.push_back( d_single_inv_map[prog] ); + progs.push_back( prog ); Trace("cegqi-si-debug2") << "subs : " << inv << " -> var for " << prog << " : " << d_single_inv_map[prog] << std::endl; } } - cr = c.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() ); + if( singleInvocation ){ + cr = c.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() ); + }else{ + cr = c; + if( invExtractPrePost ){ + if( terms.size()==1 ){ + conjuncts_si_progs.push_back( progs[0] ); + conjuncts_si_invokes.push_back( terms[0] ); + }else if( terms.size()>1 ){ + //abort when mixing multiple invariants? TODO + invExtractPrePost = false; + } + } + } }else{ cr = c; } @@ -920,6 +970,10 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) { Node curr = disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( OR, disj ); curr = TermDb::simpleNegate( curr ); Trace("cegqi-si") << " " << curr; + if( invExtractPrePost && conjuncts.size()==conjuncts_si_progs.size() ){ + conjuncts_si_progs.push_back( Node::null() ); + conjuncts_si_invokes.push_back( Node::null() ); + } conjuncts.push_back( curr ); if( !it->first.isNull() ){ Trace("cegqi-si-debug") << " under " << it->first; @@ -927,68 +981,162 @@ void CegConjectureSingleInv::initialize( QuantifiersEngine * qe, Node q ) { Trace("cegqi-si") << std::endl; } Assert( !conjuncts.empty() ); - //make the skolems for the existential - if( !it->first.isNull() ){ - std::vector< Node > vars; - std::vector< Node > sks; - for( unsigned j=0; j<it->first.getNumChildren(); j++ ){ - std::stringstream ss; - ss << "a_" << it->first[j]; - Node v = NodeManager::currentNM()->mkSkolem( ss.str(), it->first[j].getType(), "single invocation skolem" ); - vars.push_back( it->first[j] ); - sks.push_back( v ); + //CASE 1 : rewrite based on a template for invariants + if( invExtractPrePost ){ + //for invariant synthesis + std::map< Node, bool > has_inv; + std::map< Node, std::vector< Node > > inv_pre_post[2]; + for( unsigned c=0; c<conjuncts.size(); c++ ){ + Node inv = conjuncts_si_invokes[c]; + Node prog = conjuncts_si_progs[c]; + Trace("cegqi-si-inv-debug") << "Conjunct #" << c << ": " << conjuncts[c] << std::endl; + if( !prog.isNull() ){ + Trace("cegqi-si-inv-debug") << "...has program " << prog << " invoked once: " << inv << std::endl; + std::vector< Node > curr_disj; + //find the polarity of the invocation : this determines pre vs. post + int pol = extractInvariantPolarity( conjuncts[c], inv, curr_disj, true ); + Trace("cegqi-si-inv-debug") << "...polarity is " << pol << std::endl; + if( ( pol==1 && !curr_disj.empty() ) || pol==0 ){ + //conjunct is part of pre/post condition : will add to template of invariant + Node nc = curr_disj.empty() ? NodeManager::currentNM()->mkConst( true ) : + ( curr_disj.size()==1 ? curr_disj[0] : NodeManager::currentNM()->mkNode( AND, curr_disj ) ); + nc = pol==0 ? nc : TermDb::simpleNegate( nc ); + Trace("cegqi-si-inv-debug") << " -> " << nc << " is " << ( pol==0 ? "pre" : "post" ) << "condition of invariant " << prog << "." << std::endl; + inv_pre_post[pol][prog].push_back( nc ); + has_inv[prog] = true; + } + } } - //substitute conjunctions - for( unsigned i=0; i<conjuncts.size(); i++ ){ - conjuncts[i] = conjuncts[i].substitute( vars.begin(), vars.end(), sks.begin(), sks.end() ); + Trace("cegqi-si-inv") << "Constructing invariant templates..." << std::endl; + //now, contruct the template for the invariant(s) + std::map< Node, Node > prog_templ; + for( std::map< Node, bool >::iterator iti = has_inv.begin(); iti != has_inv.end(); ++iti ){ + Node prog = iti->first; + Trace("cegqi-si-inv") << "...for " << prog << "..." << std::endl; + Trace("cegqi-si-inv") << " args : "; + for( unsigned j=0; j<prog_vars[prog].size(); j++ ){ + Node v = NodeManager::currentNM()->mkBoundVar( prog_vars[prog][j].getType() ); + d_prog_templ_vars[prog].push_back( v ); + Trace("cegqi-si-inv") << v << " "; + } + Trace("cegqi-si-inv") << std::endl; + Node pre = inv_pre_post[0][prog].empty() ? NodeManager::currentNM()->mkConst( false ) : + ( inv_pre_post[0][prog].size()==1 ? inv_pre_post[0][prog][0] : NodeManager::currentNM()->mkNode( OR, inv_pre_post[0][prog] ) ); + d_trans_pre[prog] = pre.substitute( prog_vars[prog].begin(), prog_vars[prog].end(), d_prog_templ_vars[prog].begin(), d_prog_templ_vars[prog].end() ); + Node post = inv_pre_post[1][prog].empty() ? NodeManager::currentNM()->mkConst( true ) : + ( inv_pre_post[1][prog].size()==1 ? inv_pre_post[1][prog][0] : NodeManager::currentNM()->mkNode( AND, inv_pre_post[1][prog] ) ); + d_trans_post[prog] = post.substitute( prog_vars[prog].begin(), prog_vars[prog].end(), d_prog_templ_vars[prog].begin(), d_prog_templ_vars[prog].end() ); + Trace("cegqi-si-inv") << " precondition : " << d_trans_pre[prog] << std::endl; + Trace("cegqi-si-inv") << " postcondition : " << d_trans_post[prog] << std::endl; + Node invariant = d_single_inv_app_map[prog]; + invariant = invariant.substitute( prog_vars[prog].begin(), prog_vars[prog].end(), d_prog_templ_vars[prog].begin(), d_prog_templ_vars[prog].end() ); + Trace("cegqi-si-inv") << " invariant : " << invariant << std::endl; + //construct template + Node templ; + if( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_PRE ){ + //templ = NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( OR, d_trans_pre[prog], invariant ), d_trans_post[prog] ); + templ = NodeManager::currentNM()->mkNode( OR, d_trans_pre[prog], invariant ); + }else{ + Assert( options::sygusInvTemplMode() == SYGUS_INV_TEMPL_MODE_POST ); + //templ = NodeManager::currentNM()->mkNode( OR, d_trans_pre[prog], NodeManager::currentNM()->mkNode( AND, d_trans_post[prog], invariant ) ); + templ = NodeManager::currentNM()->mkNode( AND, d_trans_post[prog], invariant ); + } + Trace("cegqi-si-inv") << " template : " << templ << std::endl; + prog_templ[prog] = templ; } - d_single_inv_arg_sk.insert( d_single_inv_arg_sk.end(), sks.begin(), sks.end() ); - //substitute single invocation applications - for( std::map< Node, Node >::iterator itam = d_single_inv_app_map.begin(); itam != d_single_inv_app_map.end(); ++itam ){ - Node n = itam->second; - d_single_inv_app_map[itam->first] = n.substitute( vars.begin(), vars.end(), sks.begin(), sks.end() ); + Node bd = conjuncts.size()==1 ? conjuncts[0] : NodeManager::currentNM()->mkNode( OR, conjuncts ); + Trace("cegqi-si-inv") << " body : " << bd << std::endl; + bd = substituteInvariantTemplates( bd, prog_templ, d_prog_templ_vars ); + Trace("cegqi-si-inv-debug") << " templ-subs body : " << bd << std::endl; + //make inner existential + std::vector< Node > new_var_bv; + for( unsigned j=0; j<new_vars.size(); j++ ){ + new_var_bv.push_back( NodeManager::currentNM()->mkBoundVar( new_vars[j].getType() ) ); } - } - //ensure that this is a ground property - for( std::map< Node, Node >::iterator itam = d_single_inv_app_map.begin(); itam != d_single_inv_app_map.end(); ++itam ){ - Node n = itam->second; - //check if all variables are arguments of this - std::vector< Node > n_args; - for( unsigned i=1; i<n.getNumChildren(); i++ ){ - n_args.push_back( n[i] ); + bd = bd.substitute( new_vars.begin(), new_vars.end(), new_var_bv.begin(), new_var_bv.end() ); + for( unsigned j=0; j<q[1][0][0].getNumChildren(); j++ ){ + new_var_bv.push_back( q[1][0][0][j] ); } - for( int i=0; i<(int)d_single_inv_arg_sk.size(); i++ ){ - if( std::find( n_args.begin(), n_args.end(), d_single_inv_arg_sk[i] )==n_args.end() ){ - Trace("cegqi-si") << "...property is not ground: program invocation " << n << " does not contain variable " << d_single_inv_arg_sk[i] << "." << std::endl; - //try to do variable elimination on d_single_inv_arg_sk[i] - if( doVariableElimination( d_single_inv_arg_sk[i], conjuncts ) ){ - Trace("cegqi-si") << "...did variable elimination on " << d_single_inv_arg_sk[i] << std::endl; - d_single_inv_arg_sk.erase( d_single_inv_arg_sk.begin() + i, d_single_inv_arg_sk.begin() + i + 1 ); - i--; - }else{ - singleInvocation = false; - //exit( 57 ); + if( !new_var_bv.empty() ){ + Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, new_var_bv ); + bd = NodeManager::currentNM()->mkNode( FORALL, bvl, TermDb::simpleNegate( bd ) ).negate(); + } + //make outer universal + bd = NodeManager::currentNM()->mkNode( FORALL, q[0], bd ); + bd = Rewriter::rewrite( bd ); + Trace("cegqi-si-inv") << " rtempl-subs body : " << bd << std::endl; + d_quant = bd; + //CASE 2 : rewrite based on single invocation + }else{ + //make the skolems for the existential + if( !it->first.isNull() ){ + std::vector< Node > vars; + std::vector< Node > sks; + for( unsigned j=0; j<it->first.getNumChildren(); j++ ){ + std::stringstream ss; + ss << "a_" << it->first[j]; + Node v = NodeManager::currentNM()->mkSkolem( ss.str(), it->first[j].getType(), "single invocation skolem" ); + vars.push_back( it->first[j] ); + sks.push_back( v ); + } + //substitute conjunctions + for( unsigned i=0; i<conjuncts.size(); i++ ){ + conjuncts[i] = conjuncts[i].substitute( vars.begin(), vars.end(), sks.begin(), sks.end() ); + } + d_single_inv_arg_sk.insert( d_single_inv_arg_sk.end(), sks.begin(), sks.end() ); + //substitute single invocation applications + for( std::map< Node, Node >::iterator itam = d_single_inv_app_map.begin(); itam != d_single_inv_app_map.end(); ++itam ){ + Node n = itam->second; + d_single_inv_app_map[itam->first] = n.substitute( vars.begin(), vars.end(), sks.begin(), sks.end() ); + } + } + //ensure that this is a ground property + for( std::map< Node, Node >::iterator itam = d_single_inv_app_map.begin(); itam != d_single_inv_app_map.end(); ++itam ){ + Node n = itam->second; + //check if all variables are arguments of this + std::vector< Node > n_args; + for( unsigned i=1; i<n.getNumChildren(); i++ ){ + n_args.push_back( n[i] ); + } + for( int i=0; i<(int)d_single_inv_arg_sk.size(); i++ ){ + if( std::find( n_args.begin(), n_args.end(), d_single_inv_arg_sk[i] )==n_args.end() ){ + Trace("cegqi-si") << "...property is not ground: program invocation " << n << " does not contain variable " << d_single_inv_arg_sk[i] << "." << std::endl; + //try to do variable elimination on d_single_inv_arg_sk[i] + if( doVariableElimination( d_single_inv_arg_sk[i], conjuncts ) ){ + Trace("cegqi-si") << "...did variable elimination on " << d_single_inv_arg_sk[i] << std::endl; + d_single_inv_arg_sk.erase( d_single_inv_arg_sk.begin() + i, d_single_inv_arg_sk.begin() + i + 1 ); + i--; + }else{ + singleInvocation = false; + //exit( 57 ); + } + break; } - break; } } - } - if( singleInvocation ){ - Node bd = conjuncts.size()==1 ? conjuncts[0] : NodeManager::currentNM()->mkNode( OR, conjuncts ); - d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, bd ); - Trace("cegqi-si-debug") << "...formula is : " << d_single_inv << std::endl; - if( options::eMatching.wasSetByUser() ){ - Node bd = d_qe->getTermDatabase()->getInstConstantBody( d_single_inv ); - std::vector< Node > patTerms; - std::vector< Node > exclude; - inst::Trigger::collectPatTerms( d_qe, d_single_inv, bd, patTerms, inst::Trigger::TS_ALL, exclude ); - if( !patTerms.empty() ){ - Trace("cegqi-si-em") << "Triggers : " << std::endl; - for( unsigned i=0; i<patTerms.size(); i++ ){ - Trace("cegqi-si-em") << " " << patTerms[i] << std::endl; + if( singleInvocation ){ + Node bd = conjuncts.size()==1 ? conjuncts[0] : NodeManager::currentNM()->mkNode( OR, conjuncts ); + 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() && options::eMatching.wasSetByUser() ){ + Node bd = d_qe->getTermDatabase()->getInstConstantBody( d_single_inv ); + std::vector< Node > patTerms; + std::vector< Node > exclude; + inst::Trigger::collectPatTerms( d_qe, d_single_inv, bd, patTerms, inst::Trigger::TS_ALL, exclude ); + if( !patTerms.empty() ){ + Trace("cegqi-si-em") << "Triggers : " << std::endl; + for( unsigned i=0; i<patTerms.size(); i++ ){ + Trace("cegqi-si-em") << " " << patTerms[i] << std::endl; + } } } + */ } } } @@ -997,9 +1145,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(); + } } } @@ -1060,9 +1267,66 @@ bool CegConjectureSingleInv::getVariableEliminationTerm( bool pol, bool hasPol, return false; } +int CegConjectureSingleInv::extractInvariantPolarity( Node n, Node inv, std::vector< Node >& curr_disj, bool pol ) { + if( n.getKind()==NOT ){ + return extractInvariantPolarity( n[0], inv, curr_disj, !pol ); + }else if( ( n.getKind()==AND && pol ) || ( n.getKind()==OR && !pol ) ){ + int curr_pol = -1; + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + int eipc = extractInvariantPolarity( n[i], inv, curr_disj, pol ); + if( eipc!=-1 ){ + if( curr_pol==-1 ){ + curr_pol = eipc; + }else{ + return -1; + } + }else{ + curr_disj.push_back( pol ? n[i] : TermDb::simpleNegate( n[i] ) ); + } + } + return curr_pol; + }else if( n==inv ){ + return pol ? 1 : 0; + }else{ + return -1; + } +} + +Node CegConjectureSingleInv::substituteInvariantTemplates( Node n, std::map< Node, Node >& prog_templ, std::map< Node, std::vector< Node > >& prog_templ_vars ) { + if( n.getKind()==APPLY_UF && n.getNumChildren()>0 ){ + std::map< Node, Node >::iterator it = prog_templ.find( n[0] ); + if( it!=prog_templ.end() ){ + std::vector< Node > children; + for( unsigned i=1; i<n.getNumChildren(); i++ ){ + children.push_back( n[i] ); + } + std::map< Node, std::vector< Node > >::iterator itv = prog_templ_vars.find( n[0] ); + Assert( itv!=prog_templ_vars.end() ); + Assert( children.size()==itv->second.size() ); + Node newc = it->second.substitute( itv->second.begin(), itv->second.end(), children.begin(), children.end() ); + return newc; + } + } + bool childChanged = false; + std::vector< Node > children; + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + Node nn = substituteInvariantTemplates( n[i], prog_templ, prog_templ_vars ); + children.push_back( nn ); + childChanged = childChanged || ( nn!=n[i] ); + } + if( childChanged ){ + if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ + children.insert( children.begin(), n.getOperator() ); + } + return NodeManager::currentNM()->mkNode( n.getKind(), children ); + }else{ + return n; + } +} + bool CegConjectureSingleInv::analyzeSygusConjunct( Node p, Node n, std::map< Node, std::vector< Node > >& children, - std::map< Node, std::map< Node, std::vector< Node > > >& prog_invoke, - std::vector< Node >& progs, std::map< Node, std::map< Node, bool > >& contains, bool pol ) { + std::map< Node, std::map< Node, std::vector< Node > > >& prog_invoke, + std::vector< Node >& progs, std::map< Node, std::map< Node, bool > >& contains, bool pol ) { if( ( pol && n.getKind()==OR ) || ( !pol && n.getKind()==AND ) ){ for( unsigned i=0; i<n.getNumChildren(); i++ ){ if( !analyzeSygusConjunct( p, n[i], children, prog_invoke, progs, contains, pol ) ){ @@ -1169,8 +1433,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 ); @@ -1184,20 +1447,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() ); @@ -1223,7 +1527,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; @@ -1231,7 +1549,12 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int& Trace("csi-sol") << "Solution (pre-simplification): " << d_orig_solution << std::endl; s = d_sol->simplifySolution( s, stn ); Trace("csi-sol") << "Solution (post-simplification): " << s << std::endl; + return reconstructToSyntax( s, stn, reconstructed ); +} + +Node CegConjectureSingleInv::reconstructToSyntax( Node s, TypeNode stn, int& reconstructed ) { d_solution = s; + const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype(); //reconstruct the solution into sygus if necessary reconstructed = 0; @@ -1240,6 +1563,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; } @@ -1276,4 +1603,14 @@ 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 54f762720..f0d00b61c 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.h +++ b/src/theory/quantifiers/ce_guided_single_inv.h @@ -71,8 +71,9 @@ public: std::vector< Node > d_vars; //delta Node d_n_delta; + bool d_used_delta; //check : add instantiations based on valuation of d_vars - void check(); + bool check(); // get delta lemmas : on-demand force minimality of d_n_delta void getDeltaLemmas( std::vector< Node >& lems ); }; @@ -110,8 +111,14 @@ 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 ); + //for recognizing templates for invariant synthesis + int extractInvariantPolarity( Node n, Node inv, std::vector< Node >& curr_disj, bool pol ); + Node substituteInvariantTemplates( Node n, std::map< Node, Node >& prog_templ, std::map< Node, std::vector< Node > >& prog_templ_vars ); + //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; @@ -126,8 +133,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 @@ -135,6 +140,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 @@ -149,6 +159,10 @@ public: Node d_quant; // single invocation version of quant Node d_single_inv; + // transition relation version per program + std::map< Node, Node > d_trans_pre; + std::map< Node, Node > d_trans_post; + std::map< Node, std::vector< Node > > d_prog_templ_vars; public: //get the single invocation lemma Node getSingleInvLemma( Node guard ); @@ -158,8 +172,14 @@ public: void check( std::vector< Node >& lems ); //get solution Node getSolution( unsigned sol_index, TypeNode stn, int& reconstructed ); + //reconstruct to syntax + Node reconstructToSyntax( Node s, 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 845e20795..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 ); @@ -309,7 +318,7 @@ Node CegConjectureSingleInvSol::simplifySolution( Node sol, TypeNode stn ){ } Node sol0 = Rewriter::rewrite( sol ); Trace("csi-sol") << "now : " << sol0 << std::endl; - + Node curr_sol = sol0; Node prev_sol; do{ @@ -359,7 +368,7 @@ Node CegConjectureSingleInvSol::simplifySolution( Node sol, TypeNode stn ){ curr_sol = sol4; } }while( curr_sol!=prev_sol ); - + return curr_sol; } @@ -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() ); @@ -726,7 +735,7 @@ int CegConjectureSingleInvSol::collectReconstructNodes( Node t, TypeNode stn, in if( karg!=-1 ){ //collect the children of min_t std::vector< Node > tchildren; - if( min_t.getNumChildren()>dt[karg].getNumArgs() && d_qe->getTermDatabaseSygus()->isAssoc( min_t.getKind() ) && dt[karg].getNumArgs()==2 ){ + if( min_t.getNumChildren()>dt[karg].getNumArgs() && quantifiers::TermDb::isAssoc( min_t.getKind() ) && dt[karg].getNumArgs()==2 ){ tchildren.push_back( min_t[0] ); std::vector< Node > rem_children; for( unsigned i=1; i<min_t.getNumChildren(); i++ ){ @@ -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/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 4167c3ad9..da3c0cce0 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -281,61 +281,7 @@ TNode ConjectureGenerator::getUniversalRepresentative( TNode n, bool add ) { } Node ConjectureGenerator::getFreeVar( TypeNode tn, unsigned i ) { - Assert( !tn.isNull() ); - while( d_free_var[tn].size()<=i ){ - std::stringstream oss; - oss << tn; - std::string typ_name = oss.str(); - while( typ_name[0]=='(' ){ - typ_name.erase( typ_name.begin() ); - } - std::stringstream os; - os << typ_name[0] << i; - Node x = NodeManager::currentNM()->mkBoundVar( os.str().c_str(), tn ); - d_free_var_num[x] = d_free_var[tn].size(); - d_free_var[tn].push_back( x ); - } - return d_free_var[tn][i]; -} - - - -Node ConjectureGenerator::getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs ) { - if( n.getKind()==BOUND_VARIABLE ){ - std::map< TNode, TNode >::iterator it = subs.find( n ); - if( it==subs.end() ){ - TypeNode tn = n.getType(); - //allocate variable - unsigned vn = var_count[tn]; - var_count[tn]++; - subs[n] = getFreeVar( tn, vn ); - return subs[n]; - }else{ - return it->second; - } - }else{ - std::vector< Node > children; - if( n.getKind()!=EQUAL ){ - if( n.hasOperator() ){ - TNode op = n.getOperator(); - if( !d_tge.isRelevantFunc( op ) ){ - return Node::null(); - } - children.push_back( op ); - }else{ - return Node::null(); - } - } - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - Node cn = getCanonicalTerm( n[i], var_count, subs ); - if( cn.isNull() ){ - return Node::null(); - }else{ - children.push_back( cn ); - } - } - return NodeManager::currentNM()->mkNode( n.getKind(), children ); - } + return d_quantEngine->getTermDatabase()->getCanonicalFreeVar( tn, i ); } bool ConjectureGenerator::isHandledTerm( TNode n ){ @@ -555,11 +501,14 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) { TNode nr = q[1][r==0 ? 1 : 0]; Node eq = nl.eqNode( nr ); if( r==1 || std::find( d_conjectures.begin(), d_conjectures.end(), q )==d_conjectures.end() ){ - //must make it canonical - std::map< TypeNode, unsigned > var_count; - std::map< TNode, TNode > subs; - Trace("sg-proc-debug") << "get canonical " << eq << std::endl; - eq = getCanonicalTerm( eq, var_count, subs ); + //check if it contains only relevant functions + if( d_tge.isRelevantTerm( eq ) ){ + //make it canonical + Trace("sg-proc-debug") << "get canonical " << eq << std::endl; + eq = d_quantEngine->getTermDatabase()->getCanonicalTerm( eq ); + }else{ + eq = Node::null(); + } } if( !eq.isNull() ){ if( r==0 ){ @@ -697,7 +646,7 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) { typ_to_subs_index[it->first] = sum; sum += it->second; for( unsigned i=0; i<it->second; i++ ){ - gsubs_vars.push_back( getFreeVar( it->first, i ) ); + gsubs_vars.push_back( d_quantEngine->getTermDatabase()->getCanonicalFreeVar( it->first, i ) ); } } } @@ -993,7 +942,7 @@ unsigned ConjectureGenerator::collectFunctions( TNode opat, TNode pat, std::map< }else{ //check for max/min TypeNode tn = pat.getType(); - unsigned vn = d_free_var_num[pat]; + unsigned vn = pat.getAttribute(InstVarNumAttribute()); std::map< TypeNode, unsigned >::iterator it = mnvn.find( tn ); if( it!=mnvn.end() ){ if( vn<it->second ){ @@ -1768,15 +1717,18 @@ void TermGenEnv::collectSignatureInformation() { for( std::map< Node, TermArgTrie >::iterator it = getTermDatabase()->d_func_map_trie.begin(); it != getTermDatabase()->d_func_map_trie.end(); ++it ){ if( !getTermDatabase()->d_op_map[it->first].empty() ){ Node nn = getTermDatabase()->d_op_map[it->first][0]; + Trace("sg-rel-sig-debug") << "Check in signature : " << nn << std::endl; if( d_cg->isHandledTerm( nn ) && nn.getKind()!=APPLY_SELECTOR_TOTAL && !nn.getType().isBoolean() ){ bool do_enum = true; //check if we have enumerated ground terms if( nn.getKind()==APPLY_UF ){ + Trace("sg-rel-sig-debug") << "Check enumeration..." << std::endl; if( !d_cg->hasEnumeratedUf( nn ) ){ do_enum = false; } } if( do_enum ){ + Trace("sg-rel-sig-debug") << "Set enumeration..." << std::endl; d_funcs.push_back( it->first ); for( unsigned i=0; i<nn.getNumChildren(); i++ ){ d_func_args[it->first].push_back( nn[i].getType() ); @@ -1789,6 +1741,7 @@ void TermGenEnv::collectSignatureInformation() { getTermDatabase()->computeUfEqcTerms( it->first ); } } + Trace("sg-rel-sig-debug") << "Done check in signature : " << nn << std::endl; } } //shuffle functions @@ -2012,6 +1965,28 @@ bool TermGenEnv::considerCurrentTermCanon( unsigned tg_id ){ bool TermGenEnv::isRelevantFunc( Node f ) { return std::find( d_funcs.begin(), d_funcs.end(), f )!=d_funcs.end(); } + +bool TermGenEnv::isRelevantTerm( Node t ) { + if( t.getKind()!=BOUND_VARIABLE ){ + if( t.getKind()!=EQUAL ){ + if( t.hasOperator() ){ + TNode op = t.getOperator(); + if( !isRelevantFunc( op ) ){ + return false; + } + }else{ + return false; + } + } + for( unsigned i=0; i<t.getNumChildren(); i++ ){ + if( !isRelevantTerm( t[i] ) ){ + return false; + } + } + } + return true; +} + TermDb * TermGenEnv::getTermDatabase() { return d_cg->getTermDatabase(); } diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h index 6f99777f4..3aa932296 100644 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h @@ -171,6 +171,7 @@ public: bool considerCurrentTermCanon( unsigned tg_id ); void changeContext( bool add ); bool isRelevantFunc( Node f ); + bool isRelevantTerm( Node t ); //carry TermDb * getTermDatabase(); Node getGroundEqc( TNode r ); @@ -307,14 +308,8 @@ private: //information regarding the conjectures /** conjecture index */ TheoremIndex d_thm_index; private: //free variable list - //free variables - std::map< TypeNode, std::vector< Node > > d_free_var; - //map from free variable to FV# - std::map< TNode, unsigned > d_free_var_num; // get canonical free variable #i of type tn Node getFreeVar( TypeNode tn, unsigned i ); - // get canonical term, return null if it contains a term apart from handled signature - Node getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs ); private: //information regarding the terms //relevant patterns (the LHS's) std::map< TypeNode, std::vector< Node > > d_rel_patterns; diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 5cb8cf278..346631889 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -675,10 +675,11 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) { //check if it is a constant introduced as a representative not existing in the model's equality engine if( !d_rep_set.hasRep( tn, v ) ){ if( d_rep_set.d_type_reps.find( tn )!=d_rep_set.d_type_reps.end() && !d_rep_set.d_type_reps[ tn ].empty() ){ - //see full_model_check.cpp line 366 v = d_rep_set.d_type_reps[tn][ d_rep_set.d_type_reps[tn].size()-1 ]; }else{ - Assert( false ); + //can happen for types not involved in quantified formulas + Trace("fmc-model-func") << "No type rep for " << tn << std::endl; + v = d_qe->getTermDatabase()->getEnumerateTerm( tn, 0 ); } Trace("fmc-model-func") << "No term, assign " << v << std::endl; } diff --git a/src/theory/quantifiers/first_order_reasoning.cpp b/src/theory/quantifiers/first_order_reasoning.cpp deleted file mode 100644 index 23e18bb02..000000000 --- a/src/theory/quantifiers/first_order_reasoning.cpp +++ /dev/null @@ -1,175 +0,0 @@ -/********************* */ -/*! \file first_order_reasoning.cpp - ** \verbatim - ** Original author: Andrew Reynolds - ** Major contributors: Morgan Deters - ** 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 first order reasoning module - ** - **/ - -#include <vector> - -#include "theory/quantifiers/first_order_reasoning.h" -#include "theory/rewriter.h" -#include "proof/proof_manager.h" - -using namespace CVC4; -using namespace std; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; -using namespace CVC4::kind; - - -void FirstOrderPropagation::collectLits( Node n, std::vector<Node> & lits ){ - if( n.getKind()==FORALL ){ - collectLits( n[1], lits ); - }else if( n.getKind()==OR ){ - for(unsigned j=0; j<n.getNumChildren(); j++) { - collectLits(n[j], lits ); - } - }else{ - lits.push_back( n ); - } -} - -void FirstOrderPropagation::simplify( std::vector< Node >& assertions ){ - for( unsigned i=0; i<assertions.size(); i++) { - Trace("fo-rsn") << "Assert : " << assertions[i] << std::endl; - } - - //process all assertions - int num_processed; - int num_true = 0; - int num_rounds = 0; - do { - num_processed = 0; - for( unsigned i=0; i<assertions.size(); i++ ){ - if( d_assertion_true.find(assertions[i])==d_assertion_true.end() ){ - std::vector< Node > fo_lits; - collectLits( assertions[i], fo_lits ); - Node unitLit = process( assertions[i], fo_lits ); - if( !unitLit.isNull() ){ - Trace("fo-rsn-debug") << "...possible unit literal : " << unitLit << " from " << assertions[i] << std::endl; - bool pol = unitLit.getKind()!=NOT; - unitLit = unitLit.getKind()==NOT ? unitLit[0] : unitLit; - if( unitLit.getKind()==EQUAL ){ - - }else if( unitLit.getKind()==APPLY_UF ){ - //make sure all are unique vars; - bool success = true; - std::vector< Node > unique_vars; - for( unsigned j=0; j<unitLit.getNumChildren(); j++) { - if( unitLit[j].getKind()==BOUND_VARIABLE ){ - if( std::find(unique_vars.begin(), unique_vars.end(), unitLit[j])==unique_vars.end() ){ - unique_vars.push_back( unitLit[j] ); - }else{ - success = false; - break; - } - }else{ - success = false; - break; - } - } - if( success ){ - d_const_def[unitLit.getOperator()] = NodeManager::currentNM()->mkConst(pol); - Trace("fo-rsn") << "Propagate : " << unitLit.getOperator() << " == " << pol << std::endl; - Trace("fo-rsn") << " from : " << assertions[i] << std::endl; - d_assertion_true[assertions[i]] = true; - num_processed++; - } - }else if( unitLit.getKind()==VARIABLE ){ - d_const_def[unitLit] = NodeManager::currentNM()->mkConst(pol); - Trace("fo-rsn") << "Propagate variable : " << unitLit << " == " << pol << std::endl; - Trace("fo-rsn") << " from : " << assertions[i] << std::endl; - d_assertion_true[assertions[i]] = true; - num_processed++; - } - } - if( d_assertion_true.find(assertions[i])!=d_assertion_true.end() ){ - num_true++; - } - } - } - num_rounds++; - }while( num_processed>0 ); - Trace("fo-rsn-sum") << "Simplified " << num_true << " / " << assertions.size() << " in " << num_rounds << " rounds." << std::endl; - for( unsigned i=0; i<assertions.size(); i++ ){ - Node curr = simplify( assertions[i] ); - if( curr!=assertions[i] ){ - curr = Rewriter::rewrite( curr ); - PROOF( ProofManager::currentPM()->addDependence(curr, assertions[i]); ); - assertions[i] = curr; - } - } -} - -Node FirstOrderPropagation::process(Node a, std::vector< Node > & lits) { - int index = -1; - for( unsigned i=0; i<lits.size(); i++) { - bool pol = lits[i].getKind()!=NOT; - Node n = lits[i].getKind()==NOT ? lits[i][0] : lits[i]; - Node litDef; - if( n.getKind()==APPLY_UF ){ - if( d_const_def.find(n.getOperator())!=d_const_def.end() ){ - litDef = d_const_def[n.getOperator()]; - } - }else if( n.getKind()==VARIABLE ){ - if( d_const_def.find(n)!=d_const_def.end() ){ - litDef = d_const_def[n]; - } - } - if( !litDef.isNull() ){ - Node poln = NodeManager::currentNM()->mkConst( pol ); - if( litDef==poln ){ - Trace("fo-rsn-debug") << "Assertion " << a << " is true because of " << lits[i] << std::endl; - d_assertion_true[a] = true; - return Node::null(); - } - } - if( litDef.isNull() ){ - if( index==-1 ){ - //store undefined index - index = i; - }else{ - //two undefined, return null - return Node::null(); - } - } - } - if( index!=-1 ){ - return lits[index]; - }else{ - return Node::null(); - } -} - -Node FirstOrderPropagation::simplify( Node n ) { - if( n.getKind()==VARIABLE ){ - if( d_const_def.find(n)!=d_const_def.end() ){ - return d_const_def[n]; - } - }else if( n.getKind()==APPLY_UF ){ - if( d_const_def.find(n.getOperator())!=d_const_def.end() ){ - return d_const_def[n.getOperator()]; - } - } - if( n.getNumChildren()==0 ){ - return n; - }else{ - std::vector< Node > children; - if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ - children.push_back( n.getOperator() ); - } - for(unsigned i=0; i<n.getNumChildren(); i++) { - children.push_back( simplify(n[i]) ); - } - return NodeManager::currentNM()->mkNode( n.getKind(), children ); - } -} diff --git a/src/theory/quantifiers/first_order_reasoning.h b/src/theory/quantifiers/first_order_reasoning.h deleted file mode 100644 index 100cf34b6..000000000 --- a/src/theory/quantifiers/first_order_reasoning.h +++ /dev/null @@ -1,49 +0,0 @@ -/********************* */ -/*! \file first_order_reasoning.h - ** \verbatim - ** Original author: Andrew Reynolds - ** Major contributors: Morgan Deters - ** 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 Pre-process step for first-order reasoning - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__FIRST_ORDER_REASONING_H -#define __CVC4__FIRST_ORDER_REASONING_H - -#include <iostream> -#include <string> -#include <vector> -#include <map> -#include "expr/node.h" -#include "expr/type_node.h" - -namespace CVC4 { -namespace theory { -namespace quantifiers { - -class FirstOrderPropagation { -private: - std::map< Node, Node > d_const_def; - std::map< Node, bool > d_assertion_true; - Node process(Node a, std::vector< Node > & lits); - void collectLits( Node n, std::vector<Node> & lits ); - Node simplify( Node n ); -public: - FirstOrderPropagation(){} - ~FirstOrderPropagation(){} - - void simplify( std::vector< Node >& assertions ); -}; - -} -} -} - -#endif 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/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index 941eaf89b..f7dc709d9 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -463,13 +463,17 @@ bool VarMatchGeneratorTermSubs::getNextMatch( Node f, InstMatch& m, QuantifiersE s = Rewriter::rewrite( s ); Trace("var-trigger-matching") << "...got " << s << std::endl; d_eq_class = Node::null(); - d_rm_prev = m.get( d_var_num[0] ).isNull(); - if( !m.set( qe, d_var_num[0], s ) ){ - return false; - }else{ - if( continueNextMatch( f, m, qe ) ){ - return true; + if( s.getType().isSubtypeOf( d_var.getType() ) ){ + d_rm_prev = m.get( d_var_num[0] ).isNull(); + if( !m.set( qe, d_var_num[0], s ) ){ + return false; + }else{ + if( continueNextMatch( f, m, qe ) ){ + return true; + } } + }else{ + Trace("var-trigger-matching") << "Violates type requirement." << std::endl; } } if( d_rm_prev ){ diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index cbf0dbbd9..dab32af71 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -126,9 +126,9 @@ void InstStrategySimplex::addTermToRow( Node i, ArithVar x, Node n, NodeBuilder< } int InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){ - if( e<2 ){ + if( e<1 ){ return STATUS_UNFINISHED; - }else if( e==2 ){ + }else if( e==1 ){ if( d_quantActive.find( f )!=d_quantActive.end() ){ //the point instantiation InstMatch m_point( f ); @@ -369,12 +369,13 @@ InstStrategyCegqi::InstStrategyCegqi( QuantifiersEngine * qe ) : InstStrategy( q void InstStrategyCegqi::processResetInstantiationRound( Theory::Effort effort ) { d_check_delta_lemma = true; + d_check_delta_lemma_lc = true; } int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) { - if( e<2 ){ + if( e<1 ){ return STATUS_UNFINISHED; - }else if( e==2 ){ + }else if( e==1 ){ CegInstantiator * cinst; std::map< Node, CegInstantiator * >::iterator it = d_cinst.find( f ); if( it==d_cinst.end() ){ @@ -383,6 +384,9 @@ int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) { d_n_delta = NodeManager::currentNM()->mkSkolem( "delta", NodeManager::currentNM()->realType(), "delta for cegqi inst strategy" ); Node delta_lem = NodeManager::currentNM()->mkNode( GT, d_n_delta, NodeManager::currentNM()->mkConst( Rational( 0 ) ) ); d_quantEngine->getOutputChannel().lemma( delta_lem ); + d_n_delta_ub = NodeManager::currentNM()->mkConst( Rational(1)/Rational(1000000) ); + Node delta_lem_ub = NodeManager::currentNM()->mkNode( LT, d_n_delta, d_n_delta_ub ); + d_quantEngine->getOutputChannel().lemma( delta_lem_ub ); } cinst->d_n_delta = d_n_delta; for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){ @@ -412,8 +416,19 @@ int InstStrategyCegqi::process( Node f, Theory::Effort effort, int e ) { } Trace("inst-alg") << "-> Run cegqi for " << f << std::endl; d_curr_quant = f; - cinst->check(); + bool addedLemma = cinst->check(); + d_used_delta = d_used_delta || cinst->d_used_delta; d_curr_quant = Node::null(); + return addedLemma ? STATUS_UNKNOWN : STATUS_UNFINISHED; + }else if( e==2 ){ + if( d_check_delta_lemma_lc && d_used_delta ){ + d_check_delta_lemma_lc = false; + d_n_delta_ub = NodeManager::currentNM()->mkNode( MULT, d_n_delta_ub, d_n_delta_ub ); + d_n_delta_ub = Rewriter::rewrite( d_n_delta_ub ); + Trace("cegqi") << "Delta lemma for " << d_n_delta_ub << std::endl; + Node delta_lem_ub = NodeManager::currentNM()->mkNode( LT, d_n_delta, d_n_delta_ub ); + d_quantEngine->getOutputChannel().lemma( delta_lem_ub ); + } } return STATUS_UNKNOWN; } diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index 586cd492c..d59690c84 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -100,8 +100,11 @@ private: CegqiOutputInstStrategy * d_out; std::map< Node, CegInstantiator * > d_cinst; Node d_n_delta; + Node d_n_delta_ub; Node d_curr_quant; bool d_check_delta_lemma; + bool d_check_delta_lemma_lc; + bool d_used_delta; /** process functions */ void processResetInstantiationRound( Theory::Effort effort ); int process( Node f, Theory::Effort effort, int e ); diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index 81771c374..8958034df 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -467,12 +467,13 @@ int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){ }else{ //first, try from relevant domain RelevantDomain * rd = d_quantEngine->getRelevantDomain(); - for( unsigned r=0; r<2; r++ ){ - if( rd || r==1 ){ + unsigned rstart = options::fullSaturateQuantRd() ? 0 : 1; + for( unsigned r=rstart; r<2; r++ ){ + if( rd || r>0 ){ if( r==0 ){ Trace("inst-alg") << "-> Relevant domain instantiate " << f << "..." << std::endl; }else{ - Trace("inst-alg") << "-> Guess instantiate " << f << "..." << std::endl; + Trace("inst-alg") << "-> Ground term instantiate " << f << "..." << std::endl; } rd->compute(); unsigned final_max_i = 0; @@ -550,6 +551,7 @@ int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){ } } if( r==0 ){ + //complete guess if( d_guessed.find( f )==d_guessed.end() ){ Trace("inst-alg") << "-> Guess instantiate " << f << "..." << std::endl; d_guessed[f] = true; @@ -561,6 +563,7 @@ int InstStrategyFreeVariable::process( Node f, Theory::Effort effort, int e ){ } } } + //term enumerator? } return STATUS_UNKNOWN; } diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 4fbf298f4..631216507 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -66,11 +66,10 @@ void InstantiationEngine::finishInit(){ //counterexample-based quantifier instantiation if( options::cbqi() ){ - if( !options::cbqi2() || options::cbqi.wasSetByUser() ){ + if( !options::cbqi2() ){ d_i_splx = new InstStrategySimplex( (arith::TheoryArith*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_ARITH ), d_quantEngine ); d_instStrategies.push_back( d_i_splx ); - } - if( options::cbqi2() ){ + }else{ d_i_cegqi = new InstStrategyCegqi( d_quantEngine ); d_instStrategies.push_back( d_i_cegqi ); } diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 53f55e70b..e297e138c 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -176,7 +176,7 @@ void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) { } //if applicable, find exceptions to model via inst-gen - if( optInstGen() ){ + if( options::fmfInstGen() ){ d_didInstGen = true; d_instGenMatches = 0; d_numQuantSat = 0; @@ -201,7 +201,7 @@ void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) { }else{ d_numQuantNoSelForm++; } - if( optOneQuantPerRoundInstGen() && lems>0 ){ + if( options::fmfInstGenOneQuantPerRound() && lems>0 ){ break; } }else if( d_quant_sat.find( f )!=d_quant_sat.end() ){ @@ -341,14 +341,6 @@ bool QModelBuilderIG::hasConstantDefinition( Node n ){ return false; } -bool QModelBuilderIG::optInstGen(){ - return options::fmfInstGen(); -} - -bool QModelBuilderIG::optOneQuantPerRoundInstGen(){ - return options::fmfInstGenOneQuantPerRound(); -} - QModelBuilderIG::Statistics::Statistics(): d_num_quants_init("QModelBuilderIG::Number_Quantifiers", 0), d_num_partial_quants_init("QModelBuilderIG::Number_Partial_Quantifiers", 0), diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h index d9ed3f092..8e84f15e2 100644 --- a/src/theory/quantifiers/model_builder.h +++ b/src/theory/quantifiers/model_builder.h @@ -123,10 +123,6 @@ public: QModelBuilderIG( context::Context* c, QuantifiersEngine* qe ); virtual ~QModelBuilderIG() throw() {} public: - //whether to add inst-gen lemmas - virtual bool optInstGen(); - //whether to only consider only quantifier per round of inst-gen - virtual bool optOneQuantPerRoundInstGen(); /** statistics class */ class Statistics { public: diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index ce780a29b..2ad8be3a1 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -157,15 +157,19 @@ int ModelEngine::checkModel(){ if( it->first.isSort() ){ Trace("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl; if( Trace.isOn("model-engine-debug") ){ - Trace("model-engine-debug") << " "; - Node mbt = d_quantEngine->getTermDatabase()->getModelBasisTerm(it->first); + Trace("model-engine-debug") << " Reps : "; + for( size_t i=0; i<it->second.size(); i++ ){ + Trace("model-engine-debug") << it->second[i] << " "; + } + Trace("model-engine-debug") << std::endl; + Trace("model-engine-debug") << " Term reps : "; for( size_t i=0; i<it->second.size(); i++ ){ - //Trace("model-engine-debug") << it->second[i] << " "; Node r = d_quantEngine->getEqualityQuery()->getInternalRepresentative( it->second[i], Node::null(), 0 ); Trace("model-engine-debug") << r << " "; } Trace("model-engine-debug") << std::endl; - Trace("model-engine-debug") << " Model basis term : " << mbt << std::endl; + Node mbt = d_quantEngine->getTermDatabase()->getModelBasisTerm(it->first); + Trace("model-engine-debug") << " Basis term : " << mbt << std::endl; } } } @@ -200,6 +204,7 @@ int ModelEngine::checkModel(){ for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ Node f = fm->getAssertedQuantifier( i ); bool isAx = getTermDatabase()->isQAttrAxiom( f ); + Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << f << ", effort = " << e << "..." << std::endl; //determine if we should check this quantifier if( ( ( effort==1 && ( options::axiomInstMode()==AXIOM_INST_MODE_DEFAULT || isAx ) ) || ( effort==0 && !isAx ) ) && mb->isQuantifierActive( f ) ){ exhaustiveInstantiate( f, e ); @@ -214,7 +219,7 @@ int ModelEngine::checkModel(){ break; } }else{ - Trace("inst-fmf-ei") << "-> Inactive : " << f << std::endl; + Trace("fmf-exh-inst") << "-> Inactive : " << f << std::endl; } } } @@ -240,43 +245,46 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ mb->d_addedLemmas = 0; mb->d_incomplete_check = false; if( mb->doExhaustiveInstantiation( d_quantEngine->getModel(), f, effort ) ){ - Trace("inst-fmf-ei") << "-> Builder determined instantiation(s)." << std::endl; + Trace("fmf-exh-inst") << "-> Builder determined instantiation(s)." << std::endl; d_triedLemmas += mb->d_triedLemmas; d_addedLemmas += mb->d_addedLemmas; d_incomplete_check = d_incomplete_check || mb->d_incomplete_check; d_statistics.d_mbqi_inst_lemmas += mb->d_addedLemmas; }else{ - Trace("inst-fmf-ei") << "-> Exhaustive instantiate " << f << ", effort = " << effort << "..." << std::endl; - Debug("inst-fmf-ei") << " Instantiation Constants: "; + Trace("fmf-exh-inst-debug") << " Instantiation Constants: "; for( size_t i=0; i<f[0].getNumChildren(); i++ ){ - Debug("inst-fmf-ei") << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) << " "; + Trace("fmf-exh-inst-debug") << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) << " "; } - Debug("inst-fmf-ei") << std::endl; + Trace("fmf-exh-inst-debug") << std::endl; //create a rep set iterator and iterate over the (relevant) domain of the quantifier RepSetIterator riter( d_quantEngine, &(d_quantEngine->getModel()->d_rep_set) ); if( riter.setQuantifier( f ) ){ - Debug("inst-fmf-ei") << "Begin instantiation..." << std::endl; - int triedLemmas = 0; - int addedLemmas = 0; - while( !riter.isFinished() && ( addedLemmas==0 || !options::fmfOneInstPerRound() ) ){ - //instantiation was not shown to be true, construct the match - InstMatch m( f ); - for( int i=0; i<riter.getNumTerms(); i++ ){ - m.set( d_quantEngine, riter.d_index_order[i], riter.getTerm( i ) ); - } - Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl; - triedLemmas++; - //add as instantiation - if( d_quantEngine->addInstantiation( f, m ) ){ - addedLemmas++; - }else{ - Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl; + Trace("fmf-exh-inst") << "...exhaustive instantiation incomplete=" << riter.d_incomplete << "..." << std::endl; + if( !riter.d_incomplete || options::fmfFullSaturate() ){ + int triedLemmas = 0; + int addedLemmas = 0; + while( !riter.isFinished() && ( addedLemmas==0 || !options::fmfOneInstPerRound() ) ){ + //instantiation was not shown to be true, construct the match + InstMatch m( f ); + for( int i=0; i<riter.getNumTerms(); i++ ){ + m.set( d_quantEngine, riter.d_index_order[i], riter.getTerm( i ) ); + } + Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl; + triedLemmas++; + //add as instantiation + if( d_quantEngine->addInstantiation( f, m ) ){ + addedLemmas++; + }else{ + Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl; + } + riter.increment(); } - riter.increment(); + d_addedLemmas += addedLemmas; + d_triedLemmas += triedLemmas; + d_statistics.d_exh_inst_lemmas += addedLemmas; } - d_addedLemmas += addedLemmas; - d_triedLemmas += triedLemmas; - d_statistics.d_exh_inst_lemmas += addedLemmas; + }else{ + Assert( riter.d_incomplete ); } //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round d_incomplete_check = d_incomplete_check || riter.d_incomplete; diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h index 47cb62715..af2d88e94 100644 --- a/src/theory/quantifiers/modes.h +++ b/src/theory/quantifiers/modes.h @@ -143,6 +143,23 @@ typedef enum { TERM_DB_RELEVANT, } TermDbMode; +typedef enum { + /** do not lift ITEs in quantified formulas */ + ITE_LIFT_QUANT_MODE_NONE, + /** only lift ITEs in quantified formulas if reduces the term size */ + ITE_LIFT_QUANT_MODE_SIMPLE, + /** lift ITEs */ + ITE_LIFT_QUANT_MODE_ALL, +} IteLiftQuantMode; + +typedef enum { + /** synthesize I( x ) */ + SYGUS_INV_TEMPL_MODE_NONE, + /** synthesize ( pre( x ) V I( x ) ) */ + SYGUS_INV_TEMPL_MODE_PRE, + /** synthesize ( post( x ) ^ I( x ) ) */ + SYGUS_INV_TEMPL_MODE_POST, +} SygusInvTemplMode; }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index fe81df7f8..5cb9062e4 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -19,7 +19,7 @@ option miniscopeQuantFreeVar --miniscope-quant-fv bool :default true :read-write disable miniscope quantifiers for ground subformulas # Whether to prenex (nested universal) quantifiers option prenexQuant --prenex-quant=MODE CVC4::theory::quantifiers::PrenexQuantMode :default CVC4::theory::quantifiers::PRENEX_NO_USER_PAT :include "theory/quantifiers/modes.h" :read-write :handler CVC4::theory::quantifiers::stringToPrenexQuantMode :handler-include "theory/quantifiers/options_handlers.h" - disable prenexing of quantified formulas + prenex mode for quantified formulas # Whether to variable-eliminate quantifiers. # For example, forall x y. ( P( x, y ) V x != c ) will be rewritten to # forall y. P( c, y ) @@ -27,13 +27,16 @@ option varElimQuant --var-elim-quant bool :default true disable simple variable elimination for quantified formulas option dtVarExpandQuant --dt-var-exp-quant bool :default true expand datatype variables bound to one constructor in quantifiers +#ite lift mode for quantified formulas +option iteLiftQuant --ite-lift-quant=MODE CVC4::theory::quantifiers::IteLiftQuantMode :default CVC4::theory::quantifiers::ITE_LIFT_QUANT_MODE_SIMPLE :include "theory/quantifiers/modes.h" :read-write :handler CVC4::theory::quantifiers::stringToIteLiftQuantMode :handler-include "theory/quantifiers/options_handlers.h" + ite lifting mode for quantified formulas option iteCondVarSplitQuant --ite-cond-var-split-quant bool :default true split variables occurring as conditions of ITE in quantifiers -option simpleIteLiftQuant --ite-lift-quant bool :default true - disable simple ite lifting for quantified formulas +option iteDtTesterSplitQuant --ite-dtt-split-quant bool :read-write :default false + split ites with dt testers as conditions # Whether to CNF quantifier bodies -option cnfQuant --cnf-quant bool :default false - apply CNF conversion to quantified formulas +# option cnfQuant --cnf-quant bool :default false +# apply CNF conversion to quantified formulas # Whether to NNF quantifier bodies option nnfQuant --nnf-quant bool :default true apply NNF conversion to quantified formulas @@ -54,10 +57,10 @@ option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false # Whether to perform quantifier macro expansion option macrosQuant --macros-quant bool :default false perform quantifiers macro expansions -# Whether to perform first-order propagation -option foPropQuant --fo-prop-quant bool :default false - perform first-order propagation on quantifiers - +# Whether to CNF quantifier bodies +option elimTautQuant --elim-taut-quant bool :default true + eliminate tautological disjuncts of quantified formulas + #### E-matching options option eMatching --e-matching bool :read-write :default true @@ -83,6 +86,8 @@ option purifyDtTriggers --purify-dt-triggers bool :default false :read-write purify dt triggers, match all constructors of correct form instead of selectors option pureThTriggers --pure-th-triggers bool :default false :read-write use pure theory terms as single triggers +option partialTriggers --partial-triggers bool :default false :read-write + use triggers that do not contain all free variables option multiTriggerWhenSingle --multi-trigger-when-single bool :default false select multi triggers when single triggers exist option multiTriggerPriority --multi-trigger-priority bool :default false @@ -110,6 +115,8 @@ option eagerInstQuant --eager-inst-quant bool :default false option fullSaturateQuant --full-saturate-quant bool :default false when all other quantifier instantiation strategies fail, instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown +option fullSaturateQuantRd --full-saturate-quant-rd bool :default true + whether to use relevant domain first for full saturation instantiation strategy option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_NONE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToLiteralMatchMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkLiteralMatchMode :predicate-include "theory/quantifiers/options_handlers.h" choose literal matching mode @@ -137,8 +144,10 @@ option fmfOneQuantPerRound --mbqi-one-quant-per-round bool :default false option fmfInstEngine --fmf-inst-engine bool :default false use instantiation engine in conjunction with finite model finding +option fmfFullSaturate --fmf-full-saturate bool :default false + instantiate with all known ground terms for infinite domain quantifiers when finite model finding option fmfInstGen --fmf-inst-gen bool :default true - disable Inst-Gen instantiation techniques for finite model finding + disable Inst-Gen instantiation techniques for finite model finding option fmfInstGenOneQuantPerRound --fmf-inst-gen-one-quant-per-round bool :default false only perform Inst-Gen instantiation techniques on one quantifier per round option fmfFreshDistConst --fmf-fresh-dc bool :default false @@ -160,6 +169,8 @@ option qcfWhenMode --quant-cf-when=MODE CVC4::theory::quantifiers::QcfWhenMode : when to invoke conflict find mechanism for quantifiers option qcfTConstraint --qcf-tconstraint bool :read-write :default false enable entailment checks for t-constraints in qcf algorithm +option qcfAllConflict --qcf-all-conflict bool :read-write :default false + add all available conflicting instances during conflict-based instantiation option instNoEntail --inst-no-entail bool :read-write :default true do not consider instances of quantified formulas that are currently entailed @@ -192,7 +203,7 @@ option conjectureFilterCanonical --conjecture-filter-canonical bool :read-write filter based on canonicity option conjectureFilterModel --conjecture-filter-model bool :read-write :default true filter based on model -option conjectureGenGtEnum --conjecture-gen-gt-enum=N int :default 0 +option conjectureGenGtEnum --conjecture-gen-gt-enum=N int :default 50 number of ground terms to generate for model filtering option conjectureUeeIntro --conjecture-gen-uee-intro bool :default false more aggressive merging for universal equality engine, introduces terms @@ -209,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 @@ -225,7 +240,10 @@ option sygusNormalFormGlobalArg --sygus-nf-sym-arg bool :default true option sygusNormalFormGlobalContent --sygus-nf-sym-content bool :default true generalize based on content in global search space narrowing -# older implementation +option sygusInvTemplMode --sygus-inv-templ=MODE CVC4::theory::quantifiers::SygusInvTemplMode :default CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_NONE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToSygusInvTemplMode :handler-include "theory/quantifiers/options_handlers.h" + template mode for sygus invariant synthesis + +# approach applied to general quantified formulas option cbqi --cbqi bool :read-write :default false turns on counterexample-based quantifier instantiation option cbqi2 --cbqi2 bool :read-write :default false @@ -244,4 +262,14 @@ option ltePartialInst --lte-partial-inst bool :default false option lteRestrictInstClosure --lte-restrict-inst-closure bool :default false treat arguments of inst closure as restricted terms for instantiation +### reduction options + +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/options_handlers.h b/src/theory/quantifiers/options_handlers.h index 9fb5dd69d..4d2276621 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -204,6 +204,32 @@ relevant \n\ + Quantifiers module considers only ground terms connected to current assertions. \n\ \n\ "; +static const std::string iteLiftQuantHelp = "\ +Modes for term database, supported by --ite-lift-quant:\n\ +\n\ +all \n\ ++ Do not lift if-then-else in quantified formulas.\n\ +\n\ +simple \n\ ++ Lift if-then-else in quantified formulas if results in smaller term size.\n\ +\n\ +none \n\ ++ Lift if-then-else in quantified formulas. \n\ +\n\ +"; +static const std::string sygusInvTemplHelp = "\ +Template modes for sygus invariant synthesis, supported by --sygus-inv-templ:\n\ +\n\ +none \n\ ++ Synthesize invariant directly.\n\ +\n\ +pre \n\ ++ Synthesize invariant based on weakening of precondition .\n\ +\n\ +post \n\ ++ Synthesize invariant based on strengthening of postcondition. \n\ +\n\ +"; inline InstWhenMode stringToInstWhenMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { if(optarg == "pre-full") { @@ -414,6 +440,38 @@ inline TermDbMode stringToTermDbMode(std::string option, std::string optarg, Smt } } +inline IteLiftQuantMode stringToIteLiftQuantMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { + if(optarg == "all" ) { + return ITE_LIFT_QUANT_MODE_ALL; + } else if(optarg == "simple") { + return ITE_LIFT_QUANT_MODE_SIMPLE; + } else if(optarg == "none") { + return ITE_LIFT_QUANT_MODE_NONE; + } else if(optarg == "help") { + puts(iteLiftQuantHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --ite-lift-quant: `") + + optarg + "'. Try --ite-lift-quant help."); + } +} + +inline SygusInvTemplMode stringToSygusInvTemplMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { + if(optarg == "none" ) { + return SYGUS_INV_TEMPL_MODE_NONE; + } else if(optarg == "pre") { + return SYGUS_INV_TEMPL_MODE_PRE; + } else if(optarg == "post") { + return SYGUS_INV_TEMPL_MODE_POST; + } else if(optarg == "help") { + puts(sygusInvTemplHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --sygus-inv-templ: `") + + optarg + "'. Try --sygus-inv-templ help."); + } +} + }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 18bffe908..47c2e1c5b 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -1971,6 +1971,7 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) { Trace("qcf-debug") << std::endl; } short end_e = getMaxQcfEffort(); + bool isConflict = false; for( short e = effort_conflict; e<=end_e; e++ ){ d_effort = e; Trace("qcf-check") << "Checking quantified formulas at effort " << e << "..." << std::endl; @@ -2014,8 +2015,12 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) { ++addedLemmas; if( e==effort_conflict ){ d_quant_order.insert( d_quant_order.begin(), q ); - d_conflict.set( true ); ++(d_statistics.d_conflict_inst); + if( options::qcfAllConflict() ){ + isConflict = true; + }else{ + d_conflict.set( true ); + } break; }else if( e==effort_prop_eq ){ ++(d_statistics.d_prop_inst); @@ -2044,6 +2049,9 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) { break; } } + if( isConflict ){ + d_conflict.set( true ); + } if( Trace.isOn("qcf-engine") ){ double clSet2 = double(clock())/double(CLOCKS_PER_SEC); Trace("qcf-engine") << "Finished conflict find engine, time = " << (clSet2-clSet); diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index ca24de5f7..5e0f511e0 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -110,8 +110,6 @@ public: virtual eq::EqualityEngine* getEngine() = 0; /** get the equivalence class of a */ virtual void getEquivalenceClass( Node a, std::vector< Node >& eqc ) = 0; - - virtual void setLiberal( bool l ) = 0; };/* class EqualityQuery */ diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 0afdece82..6a95e243d 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -340,64 +340,141 @@ Node QuantifiersRewriter::computeNNF( Node body ){ } } + +void QuantifiersRewriter::computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons, + std::vector< Node >& conj ){ + if( n.getKind()==ITE && n[0].getKind()==APPLY_TESTER && n[1].getType().isBoolean() ){ + Trace("quantifiers-rewrite-ite-debug") << "Split tester condition : " << n << std::endl; + Node x = n[0][0]; + std::map< Node, Node >::iterator itp = pcons.find( x ); + if( itp!=pcons.end() ){ + Trace("quantifiers-rewrite-ite-debug") << "...condition already set " << itp->second << std::endl; + computeDtTesterIteSplit( n[ itp->second==n[0] ? 1 : 2 ], pcons, ncons, conj ); + }else{ + Expr testerExpr = n[0].getOperator().toExpr(); + int index = Datatype::indexOf( testerExpr ); + std::map< int, Node >::iterator itn = ncons[x].find( index ); + if( itn!=ncons[x].end() ){ + Trace("quantifiers-rewrite-ite-debug") << "...condition negated " << itn->second << std::endl; + computeDtTesterIteSplit( n[ 2 ], pcons, ncons, conj ); + }else{ + for( unsigned i=0; i<2; i++ ){ + if( i==0 ){ + pcons[x] = n[0]; + }else{ + pcons.erase( x ); + ncons[x][index] = n[0].negate(); + } + computeDtTesterIteSplit( n[i+1], pcons, ncons, conj ); + } + ncons[x].erase( index ); + } + } + }else{ + Trace("quantifiers-rewrite-ite-debug") << "Return value : " << n << std::endl; + std::vector< Node > children; + children.push_back( n ); + std::vector< Node > vars; + //add all positive testers + for( std::map< Node, Node >::iterator it = pcons.begin(); it != pcons.end(); ++it ){ + children.push_back( it->second.negate() ); + vars.push_back( it->first ); + } + //add all negative testers + for( std::map< Node, std::map< int, Node > >::iterator it = ncons.begin(); it != ncons.end(); ++it ){ + Node x = it->first; + //only if we haven't settled on a positive tester + if( std::find( vars.begin(), vars.end(), x )==vars.end() ){ + //check if we have exhausted all options but one + const Datatype& dt = DatatypeType(x.getType().toType()).getDatatype(); + std::vector< Node > nchildren; + int pos_cons = -1; + for( int i=0; i<(int)dt.getNumConstructors(); i++ ){ + std::map< int, Node >::iterator itt = it->second.find( i ); + if( itt==it->second.end() ){ + pos_cons = pos_cons==-1 ? i : -2; + }else{ + nchildren.push_back( itt->second.negate() ); + } + } + if( pos_cons>=0 ){ + const DatatypeConstructor& c = dt[pos_cons]; + Expr tester = c.getTester(); + children.push_back( NodeManager::currentNM()->mkNode( kind::APPLY_TESTER, Node::fromExpr( tester ), x ).negate() ); + }else{ + children.insert( children.end(), nchildren.begin(), nchildren.end() ); + } + } + } + //make condition/output pair + Node c = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children ); + conj.push_back( c ); + } +} + Node QuantifiersRewriter::computeProcessIte( Node body, bool hasPol, bool pol ) { if( body.getType().isBoolean() ){ - if( body.getKind()==EQUAL && options::simpleIteLiftQuant() ){ + if( body.getKind()==EQUAL && options::iteLiftQuant()!=ITE_LIFT_QUANT_MODE_NONE ){ for( size_t i=0; i<2; i++ ){ if( body[i].getKind()==ITE ){ Node no = i==0 ? body[1] : body[0]; - bool doRewrite = false; - std::vector< Node > children; - children.push_back( body[i][0] ); - for( size_t j=1; j<=2; j++ ){ - //check if it rewrites to a constant - Node nn = NodeManager::currentNM()->mkNode( EQUAL, no, body[i][j] ); - nn = Rewriter::rewrite( nn ); - children.push_back( nn ); - if( nn.isConst() ){ - doRewrite = true; + if( no.getKind()!=ITE ){ + bool doRewrite = options::iteLiftQuant()==ITE_LIFT_QUANT_MODE_ALL; + std::vector< Node > children; + children.push_back( body[i][0] ); + for( size_t j=1; j<=2; j++ ){ + //check if it rewrites to a constant + Node nn = NodeManager::currentNM()->mkNode( EQUAL, no, body[i][j] ); + nn = Rewriter::rewrite( nn ); + children.push_back( nn ); + if( nn.isConst() ){ + doRewrite = true; + } + } + if( doRewrite ){ + return NodeManager::currentNM()->mkNode( ITE, children ); } - } - if( doRewrite ){ - return NodeManager::currentNM()->mkNode( ITE, children ); } } } - }else if( body.getKind()==ITE && hasPol && options::iteCondVarSplitQuant() ){ - for( unsigned r=0; r<2; r++ ){ - //check if there is a variable elimination - Node b = r==0 ? body[0] : body[0].negate(); - QuantPhaseReq qpr( b ); - std::vector< Node > vars; - std::vector< Node > subs; - Trace("ite-var-split-quant") << "phase req " << body[0] << " #: " << qpr.d_phase_reqs.size() << std::endl; - for( std::map< Node, bool >::iterator it = qpr.d_phase_reqs.begin(); it != qpr.d_phase_reqs.end(); ++it ){ - Trace("ite-var-split-quant") << "phase req " << it->first << " -> " << it->second << std::endl; - if( it->second ){ - if( it->first.getKind()==EQUAL ){ - for( unsigned i=0; i<2; i++ ){ - if( it->first[i].getKind()==BOUND_VARIABLE ){ - unsigned j = i==0 ? 1 : 0; - if( !hasArg1( it->first[i], it->first[j] ) ){ - vars.push_back( it->first[i] ); - subs.push_back( it->first[j] ); - break; + }else if( body.getKind()==ITE && hasPol ){ + if( options::iteCondVarSplitQuant() ){ + Trace("quantifiers-rewrite-ite-debug") << "Conditional var eq split " << body << std::endl; + for( unsigned r=0; r<2; r++ ){ + //check if there is a variable elimination + Node b = r==0 ? body[0] : body[0].negate(); + QuantPhaseReq qpr( b ); + std::vector< Node > vars; + std::vector< Node > subs; + Trace("quantifiers-rewrite-ite-debug") << "phase req " << body[0] << " #: " << qpr.d_phase_reqs.size() << std::endl; + for( std::map< Node, bool >::iterator it = qpr.d_phase_reqs.begin(); it != qpr.d_phase_reqs.end(); ++it ){ + Trace("quantifiers-rewrite-ite-debug") << "phase req " << it->first << " -> " << it->second << std::endl; + if( it->second ){ + if( it->first.getKind()==EQUAL ){ + for( unsigned i=0; i<2; i++ ){ + if( it->first[i].getKind()==BOUND_VARIABLE ){ + unsigned j = i==0 ? 1 : 0; + if( !hasArg1( it->first[i], it->first[j] ) ){ + vars.push_back( it->first[i] ); + subs.push_back( it->first[j] ); + break; + } } } } } } - } - if( !vars.empty() ){ - //bool cpol = (r==1); - Node pos = NodeManager::currentNM()->mkNode( OR, body[0].negate(), body[1] ); - //pos = pos.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); - //pos = Rewriter::rewrite( pos ); - Node neg = NodeManager::currentNM()->mkNode( OR, body[0], body[2] ); - //Trace("ite-var-split-quant") << "Split ITE " << body << " into : " << std::endl; - //Trace("ite-var-split-quant") << " " << pos << std::endl; - //Trace("ite-var-split-quant") << " " << neg << std::endl; - return NodeManager::currentNM()->mkNode( AND, pos, neg ); + if( !vars.empty() ){ + //bool cpol = (r==1); + Node pos = NodeManager::currentNM()->mkNode( OR, body[0].negate(), body[1] ); + //pos = pos.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); + //pos = Rewriter::rewrite( pos ); + Node neg = NodeManager::currentNM()->mkNode( OR, body[0], body[2] ); + Trace("quantifiers-rewrite-ite") << "*** Split ITE (conditional variable eq) " << body << " into : " << std::endl; + Trace("quantifiers-rewrite-ite") << " " << pos << std::endl; + Trace("quantifiers-rewrite-ite") << " " << neg << std::endl; + return NodeManager::currentNM()->mkNode( AND, pos, neg ); + } } } } @@ -420,6 +497,26 @@ Node QuantifiersRewriter::computeProcessIte( Node body, bool hasPol, bool pol ) return body; } +Node QuantifiersRewriter::computeProcessIte2( Node body ){ + if( body.getKind()==ITE ){ + if( options::iteDtTesterSplitQuant() ){ + Trace("quantifiers-rewrite-ite-debug") << "DTT split : " << body << std::endl; + std::map< Node, Node > pcons; + std::map< Node, std::map< int, Node > > ncons; + std::vector< Node > conj; + computeDtTesterIteSplit( body, pcons, ncons, conj ); + Assert( !conj.empty() ); + if( conj.size()>1 ){ + Trace("quantifiers-rewrite-ite") << "*** Split ITE (datatype tester) " << body << " into : " << std::endl; + for( unsigned i=0; i<conj.size(); i++ ){ + Trace("quantifiers-rewrite-ite") << " " << conj[i] << std::endl; + } + return NodeManager::currentNM()->mkNode( AND, conj ); + } + } + } + return body; +} Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& args, Node& ipl ){ @@ -677,6 +774,30 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b } } +Node QuantifiersRewriter::computeElimTaut( Node body ) { + if( body.getKind()==OR ){ + std::vector< Node > children; + std::map< Node, bool > lit_pol; + for( unsigned i=0; i<body.getNumChildren(); i++ ){ + Node lit = body[i].getKind()==NOT ? body[i][0] : body[i]; + bool pol = body[i].getKind()!=NOT; + std::map< Node, bool >::iterator it = lit_pol.find( lit ); + if( it==lit_pol.end() ){ + lit_pol[lit] = pol; + children.push_back( body[i] ); + }else{ + if( it->second!=pol ){ + return NodeManager::currentNM()->mkConst( true ); + } + } + } + if( children.size()!=body.getNumChildren() ){ + return children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children ); + } + } + return body; +} + Node QuantifiersRewriter::computeSplit( Node f, Node body, std::vector< Node >& vars ) { if( body.getKind()==OR ){ size_t var_found_count = 0; @@ -784,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{ @@ -1002,9 +1137,13 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption }else if( computeOption==COMPUTE_NNF ){ return options::nnfQuant(); }else if( computeOption==COMPUTE_PROCESS_ITE ){ - return options::iteCondVarSplitQuant() || options::simpleIteLiftQuant(); + return options::iteLiftQuant()!=ITE_LIFT_QUANT_MODE_NONE || options::iteCondVarSplitQuant(); + }else if( computeOption==COMPUTE_PROCESS_ITE_2 ){ + return options::iteDtTesterSplitQuant(); }else if( computeOption==COMPUTE_PRENEX ){ return options::prenexQuant()!=PRENEX_NONE && !options::aggressiveMiniscopeQuant(); + }else if( computeOption==COMPUTE_ELIM_TAUT ){ + return options::elimTautQuant(); }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ return options::varElimQuant() || options::dtVarExpandQuant(); }else if( computeOption==COMPUTE_CNF ){ @@ -1041,8 +1180,12 @@ Node QuantifiersRewriter::computeOperation( Node f, bool isNested, int computeOp n = computeNNF( n ); }else if( computeOption==COMPUTE_PROCESS_ITE ){ n = computeProcessIte( n, true, true ); + }else if( computeOption==COMPUTE_PROCESS_ITE_2 ){ + n = computeProcessIte2( n ); }else if( computeOption==COMPUTE_PRENEX ){ n = computePrenex( n, args, true ); + }else if( computeOption==COMPUTE_ELIM_TAUT ){ + n = computeElimTaut( n ); }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ Node prev; do{ diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 838eff57b..d01677171 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -40,15 +40,18 @@ private: static bool hasArg( std::vector< Node >& args, Node n ); static bool hasArg1( Node a, Node n ); static Node computeClause( Node n ); + static void computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons, std::vector< Node >& conj ); private: static Node computeElimSymbols( Node body ); static Node computeMiniscoping( Node f, std::vector< Node >& args, Node body, Node ipl ); static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body ); static Node computeNNF( Node body ); static Node computeProcessIte( Node body, bool hasPol, bool pol ); + static Node computeProcessIte2( Node body ); static Node computeVarElimination( Node body, std::vector< Node >& args, Node& ipl ); static Node computeCNF( Node body, std::vector< Node >& args, NodeBuilder<>& defs, bool forcePred ); static Node computePrenex( Node body, std::vector< Node >& args, bool pol ); + static Node computeElimTaut( Node body ); static Node computeSplit( Node f, Node body, std::vector< Node >& args ); private: enum{ @@ -57,7 +60,9 @@ private: COMPUTE_AGGRESSIVE_MINISCOPING, COMPUTE_NNF, COMPUTE_PROCESS_ITE, + COMPUTE_PROCESS_ITE_2, COMPUTE_PRENEX, + COMPUTE_ELIM_TAUT, COMPUTE_VAR_ELIMINATION, //COMPUTE_FLATTEN_ARGS_UF, COMPUTE_CNF, diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 2671f616b..c6115195d 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" @@ -77,7 +78,7 @@ void TermArgTrie::debugPrint( const char * c, Node n, unsigned depth ) { } } -TermDb::TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ) : d_quantEngine( qe ), d_op_ccount( u ) { +TermDb::TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ) : d_quantEngine( qe ), d_op_ccount( u ), d_op_id_count( 0 ), d_typ_id_count( 0 ) { d_true = NodeManager::currentNM()->mkConst( true ); d_false = NodeManager::currentNM()->mkConst( false ); if( options::ceGuidedInst() ){ @@ -129,11 +130,12 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool wi bool rec = false; if( d_processed.find( n )==d_processed.end() ){ d_processed.insert(n); - d_type_map[ n.getType() ].push_back( n ); - //if this is an atomic trigger, consider adding it - //Call the children? - if( inst::Trigger::isAtomicTrigger( n ) ){ - if( !TermDb::hasInstConstAttr(n) ){ + if( !TermDb::hasInstConstAttr(n) ){ + Trace("term-db-debug") << "register term : " << n << std::endl; + d_type_map[ n.getType() ].push_back( n ); + //if this is an atomic trigger, consider adding it + //Call the children? + if( inst::Trigger::isAtomicTrigger( n ) ){ Trace("term-db") << "register term in db " << n << std::endl; Node op = getOperator( n ); /* @@ -166,7 +168,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool wi d_iclosure_processed.insert( n ); rec = true; } - if( rec ){ + if( rec && n.getKind()!=FORALL ){ for( size_t i=0; i<n.getNumChildren(); i++ ){ addTerm( n[i], added, withinQuant, withinInstClosure ); } @@ -409,7 +411,7 @@ bool TermDb::isInstClosure( Node r ) { return d_iclosure_processed.find( r )!=d_iclosure_processed.end(); } -//checks whether a type is reasonably small enough such that all of its domain elements can be enumerated +//checks whether a type is not Array and is reasonably small enough (<1000) such that all of its domain elements can be enumerated bool TermDb::mayComplete( TypeNode tn ) { std::map< TypeNode, bool >::iterator it = d_may_complete.find( tn ); if( it==d_may_complete.end() ){ @@ -779,6 +781,7 @@ Node TermDb::getCounterexampleLiteral( Node f ){ } Node TermDb::getInstConstantNode( Node n, Node f ){ + Assert( d_inst_constants.find( f )!=d_inst_constants.end() ); return convertNodeToPattern(n,f,d_vars[f],d_inst_constants[ f ]); } @@ -945,6 +948,7 @@ Node TermDb::getSkolemizedBody( Node f ){ } Node TermDb::getEnumerateTerm( TypeNode tn, unsigned index ) { + Trace("term-db-enum") << "Get enumerate term " << tn << " " << index << std::endl; std::map< TypeNode, unsigned >::iterator it = d_typ_enum_map.find( tn ); unsigned teIndex; if( it==d_typ_enum_map.end() ){ @@ -1154,6 +1158,156 @@ void TermDb::filterInstances( std::vector< Node >& nodes ){ nodes.insert( nodes.begin(), temp.begin(), temp.end() ); } +int TermDb::getIdForOperator( Node op ) { + std::map< Node, int >::iterator it = d_op_id.find( op ); + if( it==d_op_id.end() ){ + d_op_id[op] = d_op_id_count; + d_op_id_count++; + return d_op_id[op]; + }else{ + return it->second; + } +} + +int TermDb::getIdForType( TypeNode t ) { + std::map< TypeNode, int >::iterator it = d_typ_id.find( t ); + if( it==d_typ_id.end() ){ + d_typ_id[t] = d_typ_id_count; + d_typ_id_count++; + return d_typ_id[t]; + }else{ + return it->second; + } +} + +bool TermDb::getTermOrder( Node a, Node b ) { + if( a.getKind()==BOUND_VARIABLE ){ + if( b.getKind()==BOUND_VARIABLE ){ + return a.getAttribute(InstVarNumAttribute())<b.getAttribute(InstVarNumAttribute()); + }else{ + return true; + } + }else if( b.getKind()!=BOUND_VARIABLE ){ + Node aop = a.hasOperator() ? a.getOperator() : a; + Node bop = b.hasOperator() ? b.getOperator() : b; + Trace("aeq-debug2") << a << "...op..." << aop << std::endl; + Trace("aeq-debug2") << b << "...op..." << bop << std::endl; + if( aop==bop ){ + if( a.getNumChildren()==b.getNumChildren() ){ + for( unsigned i=0; i<a.getNumChildren(); i++ ){ + if( a[i]!=b[i] ){ + //first distinct child determines the ordering + return getTermOrder( a[i], b[i] ); + } + } + }else{ + return aop.getNumChildren()<bop.getNumChildren(); + } + }else{ + return getIdForOperator( aop )<getIdForOperator( bop ); + } + } + return false; +} + + + +Node TermDb::getCanonicalFreeVar( TypeNode tn, unsigned i ) { + Assert( !tn.isNull() ); + while( d_cn_free_var[tn].size()<=i ){ + std::stringstream oss; + oss << tn; + std::string typ_name = oss.str(); + while( typ_name[0]=='(' ){ + typ_name.erase( typ_name.begin() ); + } + std::stringstream os; + os << typ_name[0] << i; + Node x = NodeManager::currentNM()->mkBoundVar( os.str().c_str(), tn ); + InstVarNumAttribute ivna; + x.setAttribute(ivna,d_cn_free_var[tn].size()); + d_cn_free_var[tn].push_back( x ); + } + return d_cn_free_var[tn][i]; +} + +struct sortTermOrder { + TermDb* d_tdb; + //std::map< Node, std::map< Node, bool > > d_cache; + bool operator() (Node i, Node j) { + /* + //must consult cache since term order is partial? + std::map< Node, bool >::iterator it = d_cache[j].find( i ); + if( it!=d_cache[j].end() && it->second ){ + return false; + }else{ + bool ret = d_tdb->getTermOrder( i, j ); + d_cache[i][j] = ret; + return ret; + } + */ + return d_tdb->getTermOrder( i, j ); + } +}; + +//this function makes a canonical representation of a term ( +// - orders variables left to right +// - if apply_torder, then sort direct subterms of commutative operators +Node TermDb::getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs, bool apply_torder ) { + Trace("canon-term-debug") << "Get canonical term for " << n << std::endl; + if( n.getKind()==BOUND_VARIABLE ){ + std::map< TNode, TNode >::iterator it = subs.find( n ); + if( it==subs.end() ){ + TypeNode tn = n.getType(); + //allocate variable + unsigned vn = var_count[tn]; + var_count[tn]++; + subs[n] = getCanonicalFreeVar( tn, vn ); + Trace("canon-term-debug") << "...allocate variable." << std::endl; + return subs[n]; + }else{ + Trace("canon-term-debug") << "...return variable in subs." << std::endl; + return it->second; + } + }else if( n.getNumChildren()>0 ){ + //collect children + Trace("canon-term-debug") << "Collect children" << std::endl; + std::vector< Node > cchildren; + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + cchildren.push_back( n[i] ); + } + //if applicable, first sort by term order + if( apply_torder && isComm( n.getKind() ) ){ + Trace("canon-term-debug") << "Sort based on commutative operator " << n.getKind() << std::endl; + sortTermOrder sto; + sto.d_tdb = this; + std::sort( cchildren.begin(), cchildren.end(), sto ); + } + //now make canonical + Trace("canon-term-debug") << "Make canonical children" << std::endl; + for( unsigned i=0; i<cchildren.size(); i++ ){ + cchildren[i] = getCanonicalTerm( cchildren[i], var_count, subs, apply_torder ); + } + if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ + Trace("canon-term-debug") << "Insert operator " << n.getOperator() << std::endl; + cchildren.insert( cchildren.begin(), n.getOperator() ); + } + Trace("canon-term-debug") << "...constructing for " << n << "." << std::endl; + Node ret = NodeManager::currentNM()->mkNode( n.getKind(), cchildren ); + Trace("canon-term-debug") << "...constructed " << ret << " for " << n << "." << std::endl; + return ret; + }else{ + Trace("canon-term-debug") << "...return 0-child term." << std::endl; + return n; + } +} + +Node TermDb::getCanonicalTerm( TNode n, bool apply_torder ){ + std::map< TypeNode, unsigned > var_count; + std::map< TNode, TNode > subs; + return getCanonicalTerm( n, var_count, subs, apply_torder ); +} + bool TermDb::containsTerm( Node n, Node t ) { if( n==t ){ return true; @@ -1179,6 +1333,15 @@ Node TermDb::simpleNegate( Node n ){ } } +bool TermDb::isAssoc( Kind k ) { + return k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==IFF || + k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR || k==BITVECTOR_CONCAT; +} + +bool TermDb::isComm( Kind k ) { + return k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==IFF || + k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR; +} void TermDb::registerTrigger( theory::inst::Trigger* tr, Node op ){ if( std::find( d_op_triggers[op].begin(), d_op_triggers[op].end(), tr )==d_op_triggers[op].end() ){ @@ -1270,6 +1433,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 @@ -1417,7 +1581,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]; } @@ -1440,7 +1604,7 @@ bool TermDbSygus::getMatch2( Node p, Node n, std::map< int, Node >& s, std::vect return p==n; }else if( n.getKind()==p.getKind() && n.getNumChildren()==p.getNumChildren() ){ //try both ways? - unsigned rmax = isComm( n.getKind() ) && n.getNumChildren()==2 ? 2 : 1; + unsigned rmax = TermDb::isComm( n.getKind() ) && n.getNumChildren()==2 ? 2 : 1; std::vector< int > new_tmp; for( unsigned r=0; r<rmax; r++ ){ bool success = true; @@ -1579,7 +1743,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; */ } @@ -1591,6 +1755,7 @@ Node TermDbSygus::mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int Node TermDbSygus::sygusToBuiltin( Node n, TypeNode tn ) { std::map< Node, Node >::iterator it = d_sygus_to_builtin[tn].find( n ); if( it==d_sygus_to_builtin[tn].end() ){ + Trace("sygus-db-debug") << "SygusToBuiltin : compute for " << n << ", type = " << tn << std::endl; Assert( n.getKind()==APPLY_CONSTRUCTOR ); const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); unsigned i = Datatype::indexOf( n.getOperator().toExpr() ); @@ -1666,7 +1831,7 @@ Node TermDbSygus::builtinToSygusConst( Node c, TypeNode tn, int rcons_depth ) { int end = d_const_list[tn1].size()-d_const_list_pos[tn1]; for( int i=start; i>=end; --i ){ Node c1 = d_const_list[tn1][i]; - //only consider if smaller than c, and + //only consider if smaller than c, and if( doCompare( c1, c, ck ) ){ Node c2 = NodeManager::currentNM()->mkNode( pkm, c, c1 ); c2 = Rewriter::rewrite( c2 ); @@ -1756,28 +1921,18 @@ Node TermDbSygus::getNormalized( TypeNode t, Node prog, bool do_pre_norm, bool d } } -int TermDbSygus::getTermSize( Node n ){ +int TermDbSygus::getSygusTermSize( Node n ){ if( isVar( n ) ){ return 0; }else{ int sum = 0; for( unsigned i=0; i<n.getNumChildren(); i++ ){ - sum += getTermSize( n[i] ); + sum += getSygusTermSize( n[i] ); } return 1+sum; } } -bool TermDbSygus::isAssoc( Kind k ) { - return k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==IFF || - k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR || k==BITVECTOR_CONCAT; -} - -bool TermDbSygus::isComm( Kind k ) { - return k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==IFF || - k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR; -} - bool TermDbSygus::isAntisymmetric( Kind k, Kind& dk ) { if( k==GT ){ dk = LT; @@ -1942,10 +2097,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() ) ); @@ -1956,14 +2111,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 ); @@ -1976,7 +2131,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() ){ @@ -1986,12 +2141,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++ ){ @@ -2008,6 +2163,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 ); @@ -2197,6 +2357,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){ @@ -2216,7 +2377,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 << " "; @@ -2225,9 +2399,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; @@ -2241,23 +2416,26 @@ 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(); - for( unsigned i=0; i<dt[cIndex].getNumSygusLetArgs(); i++ ){ + 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]; std::stringstream new_str; @@ -2266,12 +2444,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 b7fa4e999..1ffe0e29e 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -149,13 +149,13 @@ public: unsigned getNumGroundTerms( Node f ); /** count number of non-redundant ground terms per operator */ std::map< Node, int > d_op_nonred_count; - /** map from APPLY_UF operators to ground terms for that operator */ + /** map from operators to ground terms for that operator */ std::map< Node, std::vector< Node > > d_op_map; /** has map */ std::map< Node, bool > d_has_map; /** map from reps to a term in eqc in d_has_map */ std::map< Node, Node > d_term_elig_eqc; - /** map from APPLY_UF functions to trie */ + /** map from operators to trie */ std::map< Node, TermArgTrie > d_func_map_trie; std::map< Node, TermArgTrie > d_func_map_eqc_trie; /**mapping from UF terms to representatives of their arguments */ @@ -326,12 +326,42 @@ public: /** filter all nodes that have instances */ void filterInstances( std::vector< Node >& nodes ); +//for term ordering +private: + /** operator id count */ + int d_op_id_count; + /** map from operators to id */ + std::map< Node, int > d_op_id; + /** type id count */ + int d_typ_id_count; + /** map from type to id */ + std::map< TypeNode, int > d_typ_id; + //free variables + std::map< TypeNode, std::vector< Node > > d_cn_free_var; + // get canonical term, return null if it contains a term apart from handled signature + Node getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs, bool apply_torder ); +public: + /** get id for operator */ + int getIdForOperator( Node op ); + /** get id for type */ + int getIdForType( TypeNode t ); + /** get term order */ + bool getTermOrder( Node a, Node b ); + /** get canonical free variable #i of type tn */ + Node getCanonicalFreeVar( TypeNode tn, unsigned i ); + /** get canonical term */ + Node getCanonicalTerm( TNode n, bool apply_torder = false ); + //general utilities public: /** simple check for contains term */ static bool containsTerm( Node n, Node t ); /** simple negate */ static Node simpleNegate( Node n ); + /** is assoc */ + static bool isAssoc( Kind k ); + /** is comm */ + static bool isComm( Kind k ); //for sygus private: @@ -403,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; @@ -425,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 ); @@ -441,10 +472,6 @@ public: void registerSygusType( TypeNode tn ); /** get arg type */ TypeNode getArgType( const DatatypeConstructor& c, int i ); - /** is assoc */ - bool isAssoc( Kind k ); - /** is comm */ - bool isComm( Kind k ); /** isAntisymmetric */ bool isAntisymmetric( Kind k, Kind& dk ); /** is idempotent arg */ @@ -459,13 +486,13 @@ 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 ); Node getSygusNormalized( Node n, std::map< TypeNode, int >& var_count, std::map< Node, Node >& subs ); Node getNormalized( TypeNode t, Node prog, bool do_pre_norm = false, bool do_post_norm = true ); - int getTermSize( Node n ); + int getSygusTermSize( Node n ); /** given a term, construct an equivalent smaller one that respects syntax */ Node minimizeBuiltinTerm( Node n ); /** given a term, expand it into more basic components */ diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index c55ed27ea..e4d9a2730 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -145,7 +145,7 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& break; } } - if( varCount<f[0].getNumChildren() ){ + if( varCount<f[0].getNumChildren() && !options::partialTriggers() ){ Trace("trigger-debug") << "Don't consider trigger since it does not contain all variables in " << f << std::endl; for( unsigned i=0; i<nodes.size(); i++) { Trace("trigger-debug") << nodes[i] << " "; @@ -226,6 +226,12 @@ bool Trigger::isUsable( Node n, Node f ){ if( isBooleanTermTrigger( n ) ){ return true; } + if( options::purifyTriggers() ){ + Node x = getInversionVariable( n ); + if( !x.isNull() ){ + return true; + } + } } return false; }else{ @@ -247,6 +253,7 @@ bool nodeContainsVar( Node n, Node v ){ } Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) { + Trace("trigger-debug") << "Is " << n << " a usable trigger?" << std::endl; if( options::relationalTriggers() ){ if( n.getKind()==EQUAL || n.getKind()==IFF || n.getKind()==GEQ ){ Node rtr; @@ -287,7 +294,7 @@ Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) { } } bool usable = quantifiers::TermDb::getInstConstAttr(n)==f && isAtomicTrigger( n ) && isUsable( n, f ); - Trace("usable") << n << " usable : " << (quantifiers::TermDb::getInstConstAttr(n)==f) << " " << isAtomicTrigger( n ) << " " << isUsable( n, f ) << std::endl; + Trace("trigger-debug") << n << " usable : " << (quantifiers::TermDb::getInstConstAttr(n)==f) << " " << isAtomicTrigger( n ) << " " << isUsable( n, f ) << std::endl; if( usable ){ return n; }else{ @@ -512,13 +519,16 @@ Node Trigger::getInversionVariable( Node n ) { if( !n[i].isConst() ){ Trace("var-trigger-debug") << "No : non-linear coefficient " << n << std::endl; return Node::null(); - }else if( n.getType().isInteger() ){ + } + /* + else if( n.getType().isInteger() ){ Rational r = n[i].getConst<Rational>(); if( r!=Rational(-1) && r!=Rational(1) ){ Trace("var-trigger-debug") << "No : not integer coefficient " << n << std::endl; return Node::null(); } } + */ } } return ret; @@ -539,8 +549,13 @@ Node Trigger::getInversion( Node n, Node x ) { x = NodeManager::currentNM()->mkNode( MINUS, x, n[i] ); }else if( n.getKind()==MULT ){ Assert( n[i].isConst() ); - Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / n[i].getConst<Rational>() ); - x = NodeManager::currentNM()->mkNode( MULT, x, coeff ); + if( x.getType().isInteger() ){ + Node coeff = NodeManager::currentNM()->mkConst( n[i].getConst<Rational>() ); + x = NodeManager::currentNM()->mkNode( INTS_DIVISION, x, coeff ); + }else{ + Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / n[i].getConst<Rational>() ); + x = NodeManager::currentNM()->mkNode( MULT, x, coeff ); + } } }else{ Assert( cindex==-1 ); diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index e654a689d..54f2a16fe 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -32,10 +32,12 @@ #include "theory/quantifiers/ce_guided_instantiation.h" #include "theory/quantifiers/local_theory_ext.h" #include "theory/quantifiers/relevant_domain.h" +#include "theory/quantifiers/alpha_equivalence.h" #include "theory/uf/options.h" #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; @@ -99,7 +101,7 @@ d_lemmas_produced_c(u){ }else{ d_model = new quantifiers::FirstOrderModelIG( this, c, "FirstOrderModelIG" ); } - if( !options::finiteModelFind() ){ + if( options::fullSaturateQuant() ){ d_rel_dom = new quantifiers::RelevantDomain( this, d_model ); }else{ d_rel_dom = NULL; @@ -163,6 +165,17 @@ d_lemmas_produced_c(u){ }else{ d_lte_part_inst = NULL; } + if( options::quantAlphaEquiv() ){ + d_alpha_equiv = new quantifiers::AlphaEquivalence( this ); + }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; @@ -202,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; } @@ -298,6 +312,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ Trace("quant-engine-debug") << " lemmas waiting = " << d_lemmas_waiting.size() << std::endl; } Trace("quant-engine-debug") << " Theory engine finished : " << !d_te->needCheck() << std::endl; + Trace("quant-engine-debug") << " Needs model effort : " << needsModelE << std::endl; Trace("quant-engine-debug") << "Resetting all modules..." << std::endl; } if( Trace.isOn("quant-engine-ee") ){ @@ -422,6 +437,38 @@ void QuantifiersEngine::check( Theory::Effort e ){ } } +bool QuantifiersEngine::reduceQuantifier( Node q ) { + std::map< Node, bool >::iterator it = d_quants_red.find( q ); + if( it==d_quants_red.end() ){ + if( d_alpha_equiv ){ + Trace("quant-engine-debug") << "Alpha equivalence " << q << "?" << std::endl; + //add equivalence with another quantified formula + if( !d_alpha_equiv->registerQuantifier( q ) ){ + Trace("quant-engine-debug") << "...alpha equivalence success." << std::endl; + ++(d_statistics.d_red_alpha_equiv); + d_quants_red[q] = true; + return true; + } + } + if( d_lte_part_inst && !q.getAttribute(LtePartialInstAttribute()) ){ + //will partially instantiate + Trace("quant-engine-debug") << "LTE: Partially instantiate " << q << "?" << std::endl; + if( d_lte_part_inst->addQuantifier( q ) ){ + Trace("quant-engine-debug") << "...LTE partially instantiate success." << std::endl; + //delayed reduction : assert to model + d_model->assertQuantifier( q, true ); + ++(d_statistics.d_red_lte_partial_inst); + d_quants_red[q] = true; + return true; + } + } + d_quants_red[q] = false; + return false; + }else{ + return it->second; + } +} + bool QuantifiersEngine::registerQuantifier( Node f ){ std::map< Node, bool >::iterator it = d_quants.find( f ); if( it==d_quants.end() ){ @@ -431,15 +478,7 @@ bool QuantifiersEngine::registerQuantifier( Node f ){ Assert( f.getKind()==FORALL ); //check whether we should apply a reduction - bool reduced = false; - if( d_lte_part_inst && !f.getAttribute(LtePartialInstAttribute()) ){ - Trace("lte-partial-inst") << "LTE: Partially instantiate " << f << "?" << std::endl; - if( d_lte_part_inst->addQuantifier( f ) ){ - reduced = true; - } - } - if( reduced ){ - d_model->assertQuantifier( f, true ); + if( reduceQuantifier( f ) ){ d_quants[f] = false; return false; }else{ @@ -482,30 +521,31 @@ void QuantifiersEngine::registerPattern( std::vector<Node> & pattern) { void QuantifiersEngine::assertQuantifier( Node f, bool pol ){ if( !pol ){ - //do skolemization - if( d_skolemized.find( f )==d_skolemized.end() ){ - Node body = d_term_db->getSkolemizedBody( f ); - NodeBuilder<> nb(kind::OR); - nb << f << body.notNode(); - Node lem = nb; - if( Trace.isOn("quantifiers-sk") ){ - Node slem = Rewriter::rewrite( lem ); - Trace("quantifiers-sk") << "Skolemize lemma : " << slem << std::endl; + //if not reduced + if( !reduceQuantifier( f ) ){ + //do skolemization + if( d_skolemized.find( f )==d_skolemized.end() ){ + Node body = d_term_db->getSkolemizedBody( f ); + NodeBuilder<> nb(kind::OR); + nb << f << body.notNode(); + Node lem = nb; + if( Trace.isOn("quantifiers-sk") ){ + Node slem = Rewriter::rewrite( lem ); + Trace("quantifiers-sk") << "Skolemize lemma : " << slem << std::endl; + } + getOutputChannel().lemma( lem, false, true ); + d_skolemized[f] = true; } - getOutputChannel().lemma( lem, false, true ); - d_skolemized[f] = true; } - } - //assert to modules TODO : handle !pol - if( pol ){ - //register the quantifier - bool nreduced = registerQuantifier( f ); - //assert it to each module - if( nreduced ){ + }else{ + //assert to modules TODO : also for !pol? + //register the quantifier, assert it to each module + if( registerQuantifier( f ) ){ d_model->assertQuantifier( f ); for( int i=0; i<(int)d_modules.size(); i++ ){ d_modules[i]->assertNode( f ); } + addTermToDatabase( d_term_db->getInstConstantBody( f ), true ); } } } @@ -714,6 +754,7 @@ Node QuantifiersEngine::getInstantiation( Node f, InstMatch& m ){ } Node QuantifiersEngine::getInstantiation( Node f, std::vector< Node >& terms ) { + d_term_db->makeInstantiationConstantsFor( f ); return getInstantiation( f, d_term_db->d_inst_constants[f], terms ); } @@ -783,12 +824,7 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bo //make it representative, this is helpful for recognizing duplication if( mkRep ){ //pick the best possible representative for instantiation, based on past use and simplicity of term - Node ti = d_eq_query->getInternalRepresentative( terms[i], f, i ); - //check if it is a subtype (can be violated in mixed int/real) FIXME : do this check inside getInternalRepresentative - if( ti.getType().isSubtypeOf( f[0][i].getType() ) ){ - terms[i] = ti; - Trace("inst-add-debug2") << " (" << terms[i] << ")"; - } + terms[i] = d_eq_query->getInternalRepresentative( terms[i], f, i ); } } Trace("inst-add-debug") << std::endl; @@ -980,7 +1016,9 @@ QuantifiersEngine::Statistics::Statistics(): d_triggers("QuantifiersEngine::Triggers", 0), d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0), d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0), - d_multi_trigger_instantiations("QuantifiersEngine::Multi_Trigger_Instantiations", 0) + d_multi_trigger_instantiations("QuantifiersEngine::Multi_Trigger_Instantiations", 0), + d_red_alpha_equiv("QuantifiersEngine::Reductions_Alpha_Equivalence", 0), + d_red_lte_partial_inst("QuantifiersEngine::Reductions_Lte_Partial_Inst", 0) { StatisticsRegistry::registerStat(&d_num_quant); StatisticsRegistry::registerStat(&d_instantiation_rounds); @@ -992,6 +1030,8 @@ QuantifiersEngine::Statistics::Statistics(): StatisticsRegistry::registerStat(&d_simple_triggers); StatisticsRegistry::registerStat(&d_multi_triggers); StatisticsRegistry::registerStat(&d_multi_trigger_instantiations); + StatisticsRegistry::registerStat(&d_red_alpha_equiv); + StatisticsRegistry::registerStat(&d_red_lte_partial_inst); } QuantifiersEngine::Statistics::~Statistics(){ @@ -1005,6 +1045,8 @@ QuantifiersEngine::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_simple_triggers); StatisticsRegistry::unregisterStat(&d_multi_triggers); StatisticsRegistry::unregisterStat(&d_multi_trigger_instantiations); + StatisticsRegistry::unregisterStat(&d_red_alpha_equiv); + StatisticsRegistry::unregisterStat(&d_red_lte_partial_inst); } eq::EqualityEngine* QuantifiersEngine::getMasterEqualityEngine(){ @@ -1070,16 +1112,12 @@ bool EqualityQueryQuantifiersEngine::areEqual( Node a, Node b ){ return true; }else{ eq::EqualityEngine* ee = getEngine(); - if( d_liberal ){ - return true;//!areDisequal( a, b ); - }else{ - if( ee->hasTerm( a ) && ee->hasTerm( b ) ){ - if( ee->areEqual( a, b ) ){ - return true; - } + if( ee->hasTerm( a ) && ee->hasTerm( b ) ){ + if( ee->areEqual( a, b ) ){ + return true; } - return false; } + return false; } } @@ -1094,6 +1132,7 @@ bool EqualityQueryQuantifiersEngine::areDisequal( Node a, Node b ){ } Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, int index ){ + Assert( f.isNull() || f.getKind()==FORALL ); Node r = getRepresentative( a ); if( !options::internalReps() ){ return r; @@ -1108,16 +1147,17 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, r = getRepresentative( r ); }else{ if( r.getType().isSort() ){ - //TODO : this can happen in rare cases - // say x:(Array Int U), select( x, 0 ), x assigned (const @u1). Trace("internal-rep-warn") << "No representative for UF constant." << std::endl; + //should never happen : UF constants should never escape model + Assert( false ); } } } } } - std::map< Node, Node >::iterator itir = d_int_rep.find( r ); - if( itir==d_int_rep.end() ){ + TypeNode v_tn = f.isNull() ? a.getType() : f[0][index].getType(); + std::map< Node, Node >::iterator itir = d_int_rep[v_tn].find( r ); + if( itir==d_int_rep[v_tn].end() ){ //find best selection for representative Node r_best; //if( options::fmfRelevantDomain() && !f.isNull() ){ @@ -1135,7 +1175,7 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, Trace("internal-rep-select") << " } " << std::endl; int r_best_score = -1; for( size_t i=0; i<eqc.size(); i++ ){ - int score = getRepScore( eqc[i], f, index ); + int score = getRepScore( eqc[i], f, index, v_tn ); if( score!=-2 ){ if( r_best.isNull() || ( score>=0 && ( r_best_score<0 || score<r_best_score ) ) ){ r_best = eqc[i]; @@ -1144,12 +1184,8 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, } } if( r_best.isNull() ){ - if( !f.isNull() ){ - Node ic = d_qe->getTermDatabase()->getInstantiationConstant( f, index ); - r_best = d_qe->getTermDatabase()->getFreeVariableForInstConstant( ic ); - }else{ - r_best = a; - } + Trace("internal-rep-warn") << "No valid choice for representative in eqc class." << std::endl; + r_best = r; } //now, make sure that no other member of the class is an instance std::hash_map<TNode, Node, TNodeHashFunction> cache; @@ -1159,7 +1195,7 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, d_rep_score[ r_best ] = d_reset_count; } Trace("internal-rep-select") << "...Choose " << r_best << std::endl; - d_int_rep[r] = r_best; + d_int_rep[v_tn][r] = r_best; if( r_best!=a ){ Trace("internal-rep-debug") << "rep( " << a << " ) = " << r << ", " << std::endl; Trace("internal-rep-debug") << "int_rep( " << a << " ) = " << r_best << ", " << std::endl; @@ -1181,8 +1217,10 @@ void EqualityQueryQuantifiersEngine::flattenRepresentatives( std::map< TypeNode, } } Trace("internal-rep-flatten") << "---Flattening representatives : " << std::endl; - for( std::map< Node, Node >::iterator it = d_int_rep.begin(); it != d_int_rep.end(); ++it ){ - Trace("internal-rep-flatten") << it->first.getType() << " : irep( " << it->first << " ) = " << it->second << std::endl; + for( std::map< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){ + for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){ + Trace("internal-rep-flatten") << itt->first << " : irep( " << it->first << " ) = " << it->second << std::endl; + } } //store representatives for newly created terms std::map< Node, Node > temp_rep_map; @@ -1190,51 +1228,55 @@ void EqualityQueryQuantifiersEngine::flattenRepresentatives( std::map< TypeNode, bool success; do { success = false; - for( std::map< Node, Node >::iterator it = d_int_rep.begin(); it != d_int_rep.end(); ++it ){ - if( it->second.getKind()==APPLY_UF && it->second.getType().isSort() ){ - Node ni = it->second; - std::vector< Node > cc; - cc.push_back( it->second.getOperator() ); - bool changed = false; - for( unsigned j=0; j<ni.getNumChildren(); j++ ){ - if( ni[j].getType().isSort() ){ - Node r = getRepresentative( ni[j] ); - if( d_int_rep.find( r )==d_int_rep.end() ){ - Assert( temp_rep_map.find( r )!=temp_rep_map.end() ); - r = temp_rep_map[r]; - } - if( r==ni ){ - //found sub-term as instance - Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to subterm " << ni[j] << std::endl; - d_int_rep[it->first] = ni[j]; + for( std::map< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){ + for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){ + if( it->second.getKind()==APPLY_UF && it->second.getType().isSort() ){ + Node ni = it->second; + std::vector< Node > cc; + cc.push_back( it->second.getOperator() ); + bool changed = false; + for( unsigned j=0; j<ni.getNumChildren(); j++ ){ + if( ni[j].getType().isSort() ){ + Node r = getRepresentative( ni[j] ); + if( itt->second.find( r )==itt->second.end() ){ + Assert( temp_rep_map.find( r )!=temp_rep_map.end() ); + r = temp_rep_map[r]; + } + if( r==ni ){ + //found sub-term as instance + Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to subterm " << ni[j] << std::endl; + itt->second[it->first] = ni[j]; + changed = false; + success = true; + break; + }else{ + Node ir = itt->second[r]; + cc.push_back( ir ); + if( ni[j]!=ir ){ + changed = true; + } + } + }else{ changed = false; - success = true; break; - }else{ - Node ir = d_int_rep[r]; - cc.push_back( ir ); - if( ni[j]!=ir ){ - changed = true; - } } - }else{ - changed = false; - break; } - } - if( changed ){ - Node n = NodeManager::currentNM()->mkNode( APPLY_UF, cc ); - Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to " << n << std::endl; - success = true; - d_int_rep[it->first] = n; - temp_rep_map[n] = it->first; + if( changed ){ + Node n = NodeManager::currentNM()->mkNode( APPLY_UF, cc ); + Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to " << n << std::endl; + success = true; + itt->second[it->first] = n; + temp_rep_map[n] = it->first; + } } } } }while( success ); Trace("internal-rep-flatten") << "---After flattening : " << std::endl; - for( std::map< Node, Node >::iterator it = d_int_rep.begin(); it != d_int_rep.end(); ++it ){ - Trace("internal-rep-flatten") << it->first.getType() << " : irep( " << it->first << " ) = " << it->second << std::endl; + for( std::map< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){ + for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){ + Trace("internal-rep-flatten") << itt->first << " : irep( " << it->first << " ) = " << it->second << std::endl; + } } } @@ -1277,6 +1319,7 @@ Node EqualityQueryQuantifiersEngine::getInstance( Node n, const std::vector< Nod } } +/* int getDepth( Node n ){ if( n.getNumChildren()==0 ){ return 0; @@ -1291,10 +1334,13 @@ int getDepth( Node n ){ return maxDepth; } } +*/ -//smaller the score, the better -int EqualityQueryQuantifiersEngine::getRepScore( Node n, Node f, int index ){ - if( options::cbqi() && quantifiers::TermDb::hasInstConstAttr(n) ){ +//-2 : invalid, -1 : undesired, otherwise : smaller the score, the better +int EqualityQueryQuantifiersEngine::getRepScore( Node n, Node f, int index, TypeNode v_tn ){ + if( options::cbqi() && quantifiers::TermDb::hasInstConstAttr(n) ){ //reject + return -2; + }else if( !n.getType().isSubtypeOf( v_tn ) ){ //reject if incorrect type return -2; }else if( options::lteRestrictInstClosure() && ( !d_qe->getTermDatabase()->isInstClosure( n ) || !d_qe->getTermDatabase()->hasTermCurrent( n, false ) ) ){ return -1; diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index d5887f907..54f63bfe0 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -92,6 +92,8 @@ namespace quantifiers { class ConjectureGenerator; class CegInstantiation; class LtePartialInst; + class AlphaEquivalence; + class FunDefEngine; }/* CVC4::theory::quantifiers */ namespace inst { @@ -119,6 +121,8 @@ private: QuantRelevance * d_quant_rel; /** relevant domain */ quantifiers::RelevantDomain* d_rel_dom; + /** alpha equivalence */ + quantifiers::AlphaEquivalence * d_alpha_equiv; /** model builder */ quantifiers::QModelBuilder* d_builder; /** phase requirements for each quantifier for each instantiation literal */ @@ -139,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, @@ -150,6 +156,8 @@ public: //effort levels private: /** list of all quantifiers seen */ std::map< Node, bool > d_quants; + /** quantifiers reduced */ + std::map< Node, bool > d_quants_red; /** list of all lemmas produced */ //std::map< Node, bool > d_lemmas_produced; BoolMap d_lemmas_produced_c; @@ -186,8 +194,7 @@ public: ~QuantifiersEngine(); /** get theory engine */ TheoryEngine* getTheoryEngine() { return d_te; } - /** get equality query object for the given type. The default is the - generic one */ + /** get equality query */ EqualityQueryQuantifiersEngine* getEqualityQuery(); /** get default sat context for quantifiers engine */ context::Context* getSatContext(); @@ -224,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; @@ -250,6 +259,8 @@ public: /** get next decision request */ Node getNextDecisionRequest(); private: + /** reduce quantifier */ + bool reduceQuantifier( Node q ); /** compute term vector */ void computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms ); /** instantiate f with arguments terms */ @@ -322,6 +333,8 @@ public: IntStat d_simple_triggers; IntStat d_multi_triggers; IntStat d_multi_trigger_instantiations; + IntStat d_red_alpha_equiv; + IntStat d_red_lte_partial_inst; Statistics(); ~Statistics(); };/* class QuantifiersEngine::Statistics */ @@ -337,20 +350,18 @@ private: /** pointer to theory engine */ QuantifiersEngine* d_qe; /** internal representatives */ - std::map< Node, Node > d_int_rep; + std::map< TypeNode, std::map< Node, Node > > d_int_rep; /** rep score */ std::map< Node, int > d_rep_score; /** reset count */ int d_reset_count; - - bool d_liberal; private: /** node contains */ Node getInstance( Node n, const std::vector< Node >& eqc, std::hash_map<TNode, Node, TNodeHashFunction>& cache ); /** get score */ - int getRepScore( Node n, Node f, int index ); + int getRepScore( Node n, Node f, int index, TypeNode v_tn ); public: - EqualityQueryQuantifiersEngine( QuantifiersEngine* qe ) : d_qe( qe ), d_reset_count( 0 ), d_liberal( false ){} + EqualityQueryQuantifiersEngine( QuantifiersEngine* qe ) : d_qe( qe ), d_reset_count( 0 ){} ~EqualityQueryQuantifiersEngine(){} /** reset */ void reset(); @@ -368,8 +379,6 @@ public: Node getInternalRepresentative( Node a, Node f, int index ); /** flatten representatives */ void flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps ); - - void setLiberal( bool l ) { d_liberal = l; } }; /* EqualityQueryQuantifiersEngine */ }/* CVC4::theory namespace */ diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index eb05564e5..6a64f762e 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -16,6 +16,7 @@ #include "theory/type_enumerator.h" #include "theory/quantifiers/bounded_integers.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/first_order_model.h" using namespace std; using namespace CVC4; @@ -187,8 +188,14 @@ bool RepSetIterator::initialize(){ TypeNode tn = d_types[i]; Trace("rsi") << "Var #" << i << " is type " << tn << "..." << std::endl; if( tn.isSort() ){ + //must ensure uninterpreted type is non-empty. if( !d_rep_set->hasType( tn ) ){ - Node var = NodeManager::currentNM()->mkSkolem( "repSet", tn, "is a variable created by the RepSetIterator" ); + //FIXME: + // terms in rep_set are now constants which mapped to terms through TheoryModel + // thus, should introduce a constant and a term. for now, just a term. + + //Node c = d_qe->getTermDatabase()->getEnumerateTerm( tn, 0 ); + Node var = d_qe->getModel()->getSomeDomainElement( tn ); Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn << std::endl; d_rep_set->add( tn, var ); } @@ -216,15 +223,18 @@ bool RepSetIterator::initialize(){ d_incomplete = true; } } - //enumerate if the sort is reasonably small, not an Array, the upper bound of 1000 is chosen arbitrarily for now + //enumerate if the sort is reasonably small }else if( d_qe->getTermDatabase()->mayComplete( tn ) ){ Trace("rsi") << " do complete, since cardinality is small (" << tn.getCardinality() << ")..." << std::endl; d_rep_set->complete( tn ); + //must have succeeded + Assert( d_rep_set->hasType( tn ) ); }else{ Trace("rsi") << " variable cannot be bounded." << std::endl; Trace("fmf-incomplete") << "Incomplete because of quantification of type " << tn << std::endl; d_incomplete = true; } + //if we have yet to determine the type of enumeration if( d_enum_type.size()<=i ){ d_enum_type.push_back( ENUM_DOMAIN_ELEMENTS ); if( d_rep_set->hasType( tn ) ){ diff --git a/src/theory/sets/theory_sets_type_enumerator.h b/src/theory/sets/theory_sets_type_enumerator.h index 551c0b0ee..fa8f108c3 100644 --- a/src/theory/sets/theory_sets_type_enumerator.h +++ b/src/theory/sets/theory_sets_type_enumerator.h @@ -62,6 +62,7 @@ public: // by the TypeEnumerator framework. SetEnumerator(const SetEnumerator& ae) throw() : TypeEnumeratorBase<SetEnumerator>(ae.d_nm->mkSetType(ae.d_constituentType)), + d_index(ae.d_index), d_constituentType(ae.d_constituentType), d_nm(ae.d_nm), d_indexVec(ae.d_indexVec), diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 52b018234..05d0c896a 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -478,6 +478,14 @@ void TheoryEngineModelBuilder::checkTerms(TNode n, TheoryModel* tm, NodeSet& cac cache.insert(n); } +void TheoryEngineModelBuilder::assignConstantRep( TheoryModel* tm, std::map<Node, Node>& constantReps, Node eqc, Node const_rep, bool fullModel ) { + constantReps[eqc] = const_rep; + Trace("model-builder") << " Assign: Setting constant rep of " << eqc << " to " << const_rep << endl; + if( !fullModel ){ + tm->d_rep_set.d_values_to_terms[const_rep] = eqc; + } +} + void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) { @@ -551,7 +559,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) if (!const_rep.isNull()) { // Theories should not specify a rep if there is already a constant in the EC Assert(rep.isNull() || rep == const_rep); - constantReps[eqc] = const_rep; + assignConstantRep( tm, constantReps, eqc, const_rep, fullModel ); typeConstSet.add(eqct.getBaseType(), const_rep); } else if (!rep.isNull()) { @@ -615,7 +623,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) Node normalized = normalize(tm, n, constantReps, true); if (normalized.isConst()) { typeConstSet.add(tb, normalized); - constantReps[*i2] = normalized; + assignConstantRep( tm, constantReps, *i2, normalized, fullModel ); Trace("model-builder") << " Eval: Setting constant rep of " << (*i2) << " to " << normalized << endl; changed = true; evaluated = true; @@ -648,7 +656,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) if (normalized.isConst()) { changed = true; typeConstSet.add(tb, normalized); - constantReps[*i] = normalized; + assignConstantRep( tm, constantReps, *i, normalized, fullModel ); assertedReps.erase(*i); i2 = i; ++i; @@ -727,11 +735,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) n = *te; } Assert(!n.isNull()); - constantReps[*i2] = n; - Trace("model-builder") << " Assign: Setting constant rep of " << (*i2) << " to " << n << endl; - if( !fullModel ){ - tm->d_rep_set.d_values_to_terms[n] = (*i2); - } + assignConstantRep( tm, constantReps, *i2, n, fullModel ); changed = true; noRepSet.erase(i2); if (assignOne) { diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index be202fb69..a161f02f4 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -261,7 +261,7 @@ protected: Node normalize(TheoryModel* m, TNode r, std::map<Node, Node>& constantReps, bool evalOnly); bool isAssignable(TNode n); void checkTerms(TNode n, TheoryModel* tm, NodeSet& cache); - + void assignConstantRep( TheoryModel* tm, std::map<Node, Node>& constantReps, Node eqc, Node const_rep, bool fullModel ); public: TheoryEngineModelBuilder(TheoryEngine* te); virtual ~TheoryEngineModelBuilder(){} |