diff options
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/conjecture_generator.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_propagator.cpp | 674 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_propagator.h | 160 | ||||
-rw-r--r-- | src/theory/quantifiers/quant_conflict_find.cpp | 148 | ||||
-rw-r--r-- | src/theory/quantifiers/quant_conflict_find.h | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/quant_util.cpp | 32 | ||||
-rw-r--r-- | src/theory/quantifiers/quant_util.h | 56 | ||||
-rw-r--r-- | src/theory/quantifiers/relevant_domain.cpp | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/relevant_domain.h | 7 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 177 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.h | 21 |
11 files changed, 1063 insertions, 220 deletions
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index beec9da3b..f8a9eefcb 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -1273,7 +1273,7 @@ bool ConjectureGenerator::notifySubstitution( TNode glhs, std::map< TNode, TNode } Trace("sg-cconj-debug") << "Evaluate RHS : : " << rhs << std::endl; //get the representative of rhs with substitution subs - TNode grhs = getTermDatabase()->evaluateTerm( rhs, subs, true ); + TNode grhs = getTermDatabase()->getEntailedTerm( rhs, subs, true ); Trace("sg-cconj-debug") << "...done evaluating term, got : " << grhs << std::endl; if( !grhs.isNull() ){ if( glhs!=grhs ){ diff --git a/src/theory/quantifiers/inst_propagator.cpp b/src/theory/quantifiers/inst_propagator.cpp new file mode 100644 index 000000000..d20f3fd4a --- /dev/null +++ b/src/theory/quantifiers/inst_propagator.cpp @@ -0,0 +1,674 @@ +/********************* */
+/*! \file inst_propagator.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** Propagate mechanism for instantiations
+ **/
+
+#include <vector>
+
+#include "theory/quantifiers/inst_propagator.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;
+
+
+EqualityQueryInstProp::EqualityQueryInstProp( QuantifiersEngine* qe ) : d_qe( qe ){
+ d_true = NodeManager::currentNM()->mkConst( true );
+ d_false = NodeManager::currentNM()->mkConst( false );
+}
+
+bool EqualityQueryInstProp::reset( Theory::Effort e ) {
+ d_uf.clear();
+ d_uf_exp.clear();
+ d_diseq_list.clear();
+ return true;
+}
+
+/** contains term */
+bool EqualityQueryInstProp::hasTerm( Node a ) {
+ if( getEngine()->hasTerm( a ) ){
+ return true;
+ }else{
+ std::vector< Node > exp;
+ Node ar = getUfRepresentative( a, exp );
+ return !ar.isNull() && getEngine()->hasTerm( ar );
+ }
+}
+
+/** get the representative of the equivalence class of a */
+Node EqualityQueryInstProp::getRepresentative( Node a ) {
+ if( getEngine()->hasTerm( a ) ){
+ a = getEngine()->getRepresentative( a );
+ }
+ std::vector< Node > exp;
+ Node ar = getUfRepresentative( a, exp );
+ return ar.isNull() ? a : ar;
+}
+
+/** returns true if a and b are equal in the current context */
+bool EqualityQueryInstProp::areEqual( Node a, Node b ) {
+ if( a==b ){
+ return true;
+ }else{
+ eq::EqualityEngine* ee = getEngine();
+ if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
+ if( ee->areEqual( a, b ) ){
+ return true;
+ }
+ }
+ return false;
+ }
+}
+
+/** returns true is a and b are disequal in the current context */
+bool EqualityQueryInstProp::areDisequal( Node a, Node b ) {
+ if( a==b ){
+ return true;
+ }else{
+ eq::EqualityEngine* ee = getEngine();
+ if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
+ if( ee->areDisequal( a, b, false ) ){
+ return true;
+ }
+ }
+ return false;
+ }
+}
+
+/** get the equality engine associated with this query */
+eq::EqualityEngine* EqualityQueryInstProp::getEngine() {
+ return d_qe->getMasterEqualityEngine();
+}
+
+/** get the equivalence class of a */
+void EqualityQueryInstProp::getEquivalenceClass( Node a, std::vector< Node >& eqc ) {
+ //TODO?
+}
+
+TNode EqualityQueryInstProp::getCongruentTerm( Node f, std::vector< TNode >& args ) {
+ TNode t = d_qe->getTermDatabase()->getCongruentTerm( f, args );
+ if( !t.isNull() ){
+ return t;
+ }else{
+ //TODO?
+ return TNode::null();
+ }
+}
+
+Node EqualityQueryInstProp::getRepresentativeExp( Node a, std::vector< Node >& exp ) {
+ bool engine_has_a = getEngine()->hasTerm( a );
+ if( engine_has_a ){
+ a = getEngine()->getRepresentative( a );
+ }
+ //get union find representative, if this occurs in the equality engine, return it
+ unsigned prev_size = exp.size();
+ Node ar = getUfRepresentative( a, exp );
+ if( !ar.isNull() ){
+ if( engine_has_a || getEngine()->hasTerm( ar ) ){
+ Assert( getEngine()->hasTerm( ar ) );
+ Assert( getEngine()->getRepresentative( ar )==ar );
+ return ar;
+ }
+ }else{
+ if( engine_has_a ){
+ return a;
+ }
+ }
+ //retract explanation
+ while( exp.size()>prev_size ){
+ exp.pop_back();
+ }
+ return Node::null();
+}
+
+bool EqualityQueryInstProp::areEqualExp( Node a, Node b, std::vector< Node >& exp ) {
+ if( areEqual( a, b ) ){
+ return true;
+ }else{
+ std::vector< Node > exp_a;
+ Node ar = getUfRepresentative( a, exp_a );
+ if( !ar.isNull() ){
+ std::vector< Node > exp_b;
+ if( ar==getUfRepresentative( b, exp_b ) ){
+ merge_exp( exp, exp_a );
+ merge_exp( exp, exp_b );
+ return true;
+ }
+ }
+ return false;
+ }
+}
+
+bool EqualityQueryInstProp::areDisequalExp( Node a, Node b, std::vector< Node >& exp ) {
+ if( areDisequal( a, b ) ){
+ return true;
+ }else{
+ //TODO?
+ return false;
+ }
+}
+
+Node EqualityQueryInstProp::getUfRepresentative( Node a, std::vector< Node >& exp ) {
+ Assert( exp.empty() );
+ std::map< Node, Node >::iterator it = d_uf.find( a );
+ if( it!=d_uf.end() ){
+ if( it->second==a ){
+ Assert( d_uf_exp[ a ].empty() );
+ return it->second;
+ }else{
+ Node m = getUfRepresentative( it->second, exp );
+ Assert( !m.isNull() );
+ if( m!=it->second ){
+ //update union find
+ d_uf[ a ] = m;
+ //update explanation : merge the explanation of the parent
+ merge_exp( d_uf_exp[ a ], exp );
+ Trace("qip-eq") << "EqualityQueryInstProp::getUfRepresentative : merge " << a << " -> " << m << ", exp size=" << d_uf_exp[ a ].size() << std::endl;
+ }
+ //add current explanation to exp: note that exp is a subset of d_uf_exp[ a ], reset
+ exp.clear();
+ exp.insert( exp.end(), d_uf_exp[ a ].begin(), d_uf_exp[ a ].end() );
+ return m;
+ }
+ }else{
+ return Node::null();
+ }
+}
+
+// set a == b with reason, return status, modify a and b to representatives pre-merge
+int EqualityQueryInstProp::setEqual( Node& a, Node& b, std::vector< Node >& reason ) {
+ int status = STATUS_MERGED_UNKNOWN;
+ Trace("qip-eq") << "EqualityQueryInstProp::setEqual " << a << ", " << b << ", reason size = " << reason.size() << std::endl;
+ //get the representative for a
+ std::vector< Node > exp_a;
+ Node ar = getUfRepresentative( a, exp_a );
+ if( ar.isNull() ){
+ Assert( exp_a.empty() );
+ ar = a;
+ }
+ if( ar==b ){
+ Trace("qip-eq") << "EqualityQueryInstProp::setEqual : already equal" << std::endl;
+ return STATUS_NONE;
+ }
+ bool swap = false;
+ //get the representative for b
+ std::vector< Node > exp_b;
+ Node br = getUfRepresentative( b, exp_b );
+ if( br.isNull() ){
+ Assert( exp_b.empty() );
+ br = b;
+ if( !getEngine()->hasTerm( br ) ){
+ if( ar!=a ){
+ swap = true;
+ }
+ }else{
+ if( getEngine()->hasTerm( ar ) ){
+ status = STATUS_MERGED_KNOWN;
+ }
+ }
+ }else{
+ if( ar==br ){
+ Trace("qip-eq") << "EqualityQueryInstProp::setEqual : already equal" << std::endl;
+ return STATUS_NONE;
+ }else if( getEngine()->hasTerm( ar ) ){
+ if( getEngine()->hasTerm( br ) ){
+ status = STATUS_MERGED_KNOWN;
+ }else{
+ swap = true;
+ }
+ }
+ }
+ if( swap ){
+ //swap
+ Node temp_r = ar;
+ ar = br;
+ br = temp_r;
+ }
+
+ Assert( ar!=br );
+ Assert( !getEngine()->hasTerm( ar ) || getEngine()->hasTerm( br ) );
+
+ //update the union find
+ Assert( d_uf_exp[ar].empty() );
+ Assert( d_uf_exp[br].empty() );
+
+ d_uf[ar] = br;
+ merge_exp( d_uf_exp[ar], exp_a );
+ merge_exp( d_uf_exp[ar], exp_b );
+ merge_exp( d_uf_exp[ar], reason );
+
+ d_uf[br] = br;
+ d_uf_exp[br].clear();
+
+ Trace("qip-eq") << "EqualityQueryInstProp::setEqual : merge " << ar << " -> " << br << ", exp size = " << d_uf_exp[ar].size() << ", status = " << status << std::endl;
+ a = ar;
+ b = br;
+ return status;
+}
+
+
+void EqualityQueryInstProp::addArgument( std::vector< TNode >& args, std::vector< TNode >& props, Node n, bool is_prop, bool pol ) {
+ if( is_prop ){
+ if( isLiteral( n ) ){
+ props.push_back( pol ? n : n.negate() );
+ return;
+ }
+ }
+ args.push_back( n );
+}
+
+bool EqualityQueryInstProp::isLiteral( Node n ) {
+ Kind ak = n.getKind()==NOT ? n[0].getKind() : n.getKind();
+ Assert( ak!=NOT );
+ return ak!=AND && ak!=OR && ak!=IFF && ak!=ITE;
+}
+
+//this is identical to TermDb::evaluateTerm2, but tracks more information
+Node EqualityQueryInstProp::evaluateTermExp( TNode n, std::vector< Node >& exp, std::map< TNode, Node >& visited, bool hasPol, bool pol,
+ std::map< Node, bool >& watch_list_out, std::vector< TNode >& props ) {
+ std::map< TNode, Node >::iterator itv = visited.find( n );
+ if( itv != visited.end() ){
+ return itv->second;
+ }else{
+ Trace("term-db-eval") << "evaluate term : " << n << std::endl;
+ std::vector< Node > exp_n;
+ Node ret = getRepresentativeExp( n, exp_n );
+ if( ret.isNull() ){
+ //term is not known to be equal to a representative in equality engine, evaluate it
+ Kind k = n.getKind();
+ if( k==FORALL ){
+ ret = Node::null();
+ }else{
+ std::map< Node, bool > watch_list_out_curr;
+ TNode f = d_qe->getTermDatabase()->getMatchOperator( n );
+ std::vector< TNode > args;
+ bool ret_set = false;
+ bool childChanged = false;
+ int abort_i = -1;
+ //get the child entailed polarity
+ Assert( n.getKind()!=IMPLIES );
+ bool newHasPol, newPol;
+ QuantPhaseReq::getEntailPolarity( n, 0, hasPol, pol, newHasPol, newPol );
+ //for each child
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ TNode c = evaluateTermExp( n[i], exp, visited, newHasPol, newPol, watch_list_out_curr, props );
+ if( c.isNull() ){
+ ret = Node::null();
+ ret_set = true;
+ break;
+ }else if( c==d_true || c==d_false ){
+ //short-circuiting
+ if( k==kind::AND || k==kind::OR ){
+ if( (k==kind::AND)==(c==d_false) ){
+ ret = c;
+ ret_set = true;
+ break;
+ }else{
+ //redundant
+ c = Node::null();
+ childChanged = true;
+ }
+ }else if( k==kind::ITE && i==0 ){
+ Assert( watch_list_out_curr.empty() );
+ ret = evaluateTermExp( n[ c==d_true ? 1 : 2], exp, visited, hasPol, pol, watch_list_out_curr, props );
+ ret_set = true;
+ break;
+ }else if( k==kind::NOT ){
+ ret = c==d_true ? d_false : d_true;
+ ret_set = true;
+ break;
+ }
+ }
+ if( !c.isNull() ){
+ childChanged = childChanged || n[i]!=c;
+ if( !f.isNull() && !watch_list_out_curr.empty() ){
+ // we are done if this is an UF application and an argument is unevaluated
+ args.push_back( c );
+ abort_i = i;
+ break;
+ }else if( ( k==kind::AND || k==kind::OR ) ){
+ if( c.getKind()==k ){
+ //flatten
+ for( unsigned j=0; j<c.getNumChildren(); j++ ){
+ addArgument( args, props, c[j], newHasPol, newPol );
+ }
+ }else{
+ addArgument( args, props, c, newHasPol, newPol );
+ }
+ //if we are in a branching position
+ if( hasPol && !newHasPol && args.size()>=2 ){
+ //we are done if at least two args are unevaluated
+ abort_i = i;
+ break;
+ }
+ }else if( k==kind::ITE ){
+ //we are done if we are ITE and condition is unevaluated
+ Assert( i==0 );
+ args.push_back( c );
+ abort_i = i;
+ break;
+ }else{
+ args.push_back( c );
+ }
+ }
+ }
+ //add remaining children if we aborted
+ if( abort_i!=-1 ){
+ for( int i=(abort_i+1); i<(int)n.getNumChildren(); i++ ){
+ args.push_back( n[i] );
+ }
+ }
+ //copy over the watch list
+ for( std::map< Node, bool >::iterator itc = watch_list_out_curr.begin(); itc != watch_list_out_curr.end(); ++itc ){
+ watch_list_out[itc->first] = itc->second;
+ }
+
+ //if we have not short-circuited evaluation
+ if( !ret_set ){
+ //if it is an indexed term, return the congruent term
+ if( !f.isNull() && watch_list_out.empty() ){
+ Assert( args.size()==n.getNumChildren() );
+ //args contains terms known by the equality engine
+ TNode nn = getCongruentTerm( f, args );
+ Trace("term-db-eval") << " got congruent term " << nn << " from DB for " << n << std::endl;
+ if( !nn.isNull() ){
+ //successfully constructed representative in EE
+ Assert( exp_n.empty() );
+ ret = getRepresentativeExp( nn, exp_n );
+ Trace("term-db-eval") << "return rep, exp size = " << exp_n.size() << std::endl;
+ merge_exp( exp, exp_n );
+ ret_set = true;
+ Assert( !ret.isNull() );
+ }
+ }
+ if( !ret_set ){
+ if( childChanged ){
+ Trace("term-db-eval") << "return rewrite" << std::endl;
+ if( ( k==kind::AND || k==kind::OR ) ){
+ if( args.empty() ){
+ ret = k==kind::AND ? d_true : d_false;
+ ret_set = true;
+ }else if( args.size()==1 ){
+ ret = args[0];
+ ret_set = true;
+ }
+ }
+ if( !ret_set ){
+ Assert( args.size()==n.getNumChildren() );
+ if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+ args.insert( args.begin(), n.getOperator() );
+ }
+ ret = NodeManager::currentNM()->mkNode( k, args );
+ ret = Rewriter::rewrite( ret );
+ watch_list_out[ret] = true;
+ }
+ }else{
+ ret = n;
+ watch_list_out[ret] = true;
+ }
+ }
+ }
+ }
+ }else{
+ Trace("term-db-eval") << "...exists in ee, return rep, exp size = " << exp_n.size() << std::endl;
+ merge_exp( exp, exp_n );
+ }
+ Trace("term-db-eval") << "evaluated term : " << n << ", got : " << ret << ", exp size = " << exp.size() << std::endl;
+ visited[n] = ret;
+ return ret;
+ }
+}
+
+void EqualityQueryInstProp::merge_exp( std::vector< Node >& v, std::vector< Node >& v_to_merge, int up_to_size ) {
+ //TODO : optimize
+ if( v.empty() ){
+ Assert( up_to_size==-1 || up_to_size==(int)v_to_merge.size() );
+ v.insert( v.end(), v_to_merge.begin(), v_to_merge.end() );
+ }else{
+ //std::vector< Node >::iterator v_end = v.end();
+ up_to_size = up_to_size==-1 ? (int)v_to_merge.size() : up_to_size;
+ for( int j=0; j<up_to_size; j++ ){
+ if( std::find( v.begin(), v.end(), v_to_merge[j] )==v.end() ){
+ v.push_back( v_to_merge[j] );
+ }
+ }
+ }
+}
+
+
+void InstPropagator::InstInfo::init( Node q, Node lem, std::vector< Node >& terms, Node body ) {
+ d_active = true;
+ //information about the instance
+ d_q = q;
+ d_lem = lem;
+ Assert( d_terms.empty() );
+ d_terms.insert( d_terms.end(), terms.begin(), terms.end() );
+ //the current lemma
+ d_curr = body;
+ d_curr_exp.push_back( body );
+}
+
+InstPropagator::InstPropagator( QuantifiersEngine* qe ) :
+d_qe( qe ), d_notify(*this), d_qy( qe ){
+}
+
+bool InstPropagator::reset( Theory::Effort e ) {
+ d_icount = 0;
+ d_ii.clear();
+ for( unsigned i=0; i<2; i++ ){
+ d_conc_to_id[i].clear();
+ }
+ d_conflict = false;
+ d_watch_list.clear();
+ d_relevant_inst.clear();
+ return d_qy.reset( e );
+}
+
+void InstPropagator::notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) {
+ if( !d_conflict ){
+ if( Trace.isOn("qip-prop") ){
+ Trace("qip-prop") << "InstPropagator:: Notify instantiation " << q << " : " << std::endl;
+ for( unsigned i=0; i<terms.size(); i++ ){
+ Trace("qip-prop") << " " << terms[i] << std::endl;
+ }
+ }
+ unsigned id = d_icount;
+ d_icount++;
+ Trace("qip-prop") << "...assign id=" << id << std::endl;
+ d_ii[id].init( q, lem, terms, body );
+ //initialize the information
+ if( cacheConclusion( id, body ) ){
+ Assert( d_update_list.empty() );
+ d_update_list.push_back( id );
+ bool firstTime = true;
+ //update infos in the update list until empty
+ do {
+ unsigned uid = d_update_list.back();
+ d_update_list.pop_back();
+ if( d_ii[uid].d_active ){
+ update( uid, d_ii[uid], firstTime );
+ }
+ firstTime = false;
+ }while( !d_update_list.empty() );
+ }else{
+ d_ii[id].d_active = false;
+ Trace("qip-prop") << "...duplicate." << std::endl;
+ }
+ }
+}
+
+bool InstPropagator::update( unsigned id, InstInfo& ii, bool firstTime ) {
+ Assert( !d_conflict );
+ Assert( ii.d_active );
+ Trace("qip-prop-debug") << "Update info [" << id << "]..." << std::endl;
+ //update the evaluation of the current lemma
+ std::map< TNode, Node > visited;
+ std::map< Node, bool > watch_list;
+ std::vector< TNode > props;
+ Node eval = d_qy.evaluateTermExp( ii.d_curr, ii.d_curr_exp, visited, true, true, watch_list, props );
+ if( eval.isNull() ){
+ ii.d_active = false;
+ }else if( firstTime || eval!=ii.d_curr ){
+ if( EqualityQueryInstProp::isLiteral( eval ) ){
+ props.push_back( eval );
+ eval = d_qy.d_true;
+ watch_list.clear();
+ }
+ if( Trace.isOn("qip-prop") ){
+ Trace("qip-prop") << "Update info [" << id << "]..." << std::endl;
+ Trace("qip-prop") << "...updated lemma " << ii.d_curr << " -> " << eval << ", exp = ";
+ debugPrintExplanation( ii.d_curr_exp, "qip-prop" );
+ Trace("qip-prop") << std::endl;
+ Trace("qip-prop") << "...watch list: " << std::endl;
+ for( std::map< Node, bool >::iterator itw = watch_list.begin(); itw!=watch_list.end(); ++itw ){
+ Trace("qip-prop") << " " << itw->first << std::endl;
+ }
+ Trace("qip-prop") << "...new propagations: " << std::endl;
+ for( unsigned i=0; i<props.size(); i++ ){
+ Trace("qip-prop") << " " << props[i] << std::endl;
+ }
+ Trace("qip-prop") << std::endl;
+ }
+ //determine the status of eval
+ if( eval==d_qy.d_false ){
+ Assert( props.empty() );
+ //we have inferred a conflict
+ conflict( ii.d_curr_exp );
+ return false;
+ }else{
+ for( unsigned i=0; i<props.size(); i++ ){
+ //if we haven't propagated this literal yet
+ if( cacheConclusion( id, props[i], 1 ) ){
+ Node lit = props[i].getKind()==NOT ? props[i][0] : props[i];
+ bool pol = props[i].getKind()!=NOT;
+ if( lit.getKind()==EQUAL ){
+ propagate( lit[0], lit[1], pol, ii.d_curr_exp );
+ }else{
+ propagate( lit, pol ? d_qy.d_true : d_qy.d_false, true, ii.d_curr_exp );
+ }
+ if( d_conflict ){
+ return false;
+ }
+ }
+ }
+ //if we have not inferred this conclusion yet
+ if( cacheConclusion( id, eval ) ){
+ ii.d_curr = eval;
+ //update the watch list
+ Trace("qip-prop-debug") << "...updating watch list for [" << id << "], curr is " << ii.d_curr << std::endl;
+ //Here, we need to be notified of enough terms such that if we are not notified, then update( ii ) will return no propagations.
+ // Similar to two-watched literals, but since we are in UF, we need to watch all terms on a complete path of two terms.
+ for( std::map< Node, bool >::iterator itw = watch_list.begin(); itw != watch_list.end(); ++itw ){
+ d_watch_list[ itw->first ][ id ] = true;
+ }
+ }else{
+ Trace("qip-prop-debug") << "...conclusion is duplicate." << std::endl;
+ ii.d_active = false;
+ }
+ }
+ }else{
+ Trace("qip-prop-debug") << "...did not update." << std::endl;
+ }
+ Assert( !d_conflict );
+ return true;
+}
+
+void InstPropagator::propagate( Node a, Node b, bool pol, std::vector< Node >& exp ) {
+ if( Trace.isOn("qip-propagate") ){
+ Trace("qip-propagate") << "* Propagate " << a << ( pol ? " == " : " != " ) << b << ", exp = ";
+ debugPrintExplanation( exp, "qip-propagate" );
+ Trace("qip-propagate") << "..." << std::endl;
+ }
+ if( pol ){
+ std::vector< Node > exp_d;
+ if( d_qy.areDisequalExp( a, b, exp_d ) ){
+ Trace("qip-prop-debug") << "...conflict." << std::endl;
+ EqualityQueryInstProp::merge_exp( exp, exp_d );
+ conflict( exp );
+ }else{
+ //set equal
+ int status = d_qy.setEqual( a, b, exp );
+ if( status==EqualityQueryInstProp::STATUS_NONE ){
+ Trace("qip-prop-debug") << "...already equal." << std::endl;
+ return;
+ }else if( status==EqualityQueryInstProp::STATUS_MERGED_KNOWN ){
+ Assert( d_qy.getEngine()->hasTerm( a ) );
+ Assert( d_qy.getEngine()->hasTerm( b ) );
+ Trace("qip-prop-debug") << "...equality between known terms." << std::endl;
+ addRelevantInstances( exp, "qip-propagate" );
+ }
+ Trace("qip-prop-debug") << "...merging " << a << " and " << b << std::endl;
+ for( unsigned i=0; i<2; i++ ){
+ //update terms from watched lists
+ Node c = i==0 ? a : b;
+ std::map< Node, std::map< unsigned, bool > >::iterator it = d_watch_list.find( c );
+ if( it!=d_watch_list.end() ){
+ Trace("qip-prop-debug") << "...update ids from watch list of " << c << ", size=" << it->second.size() << "..." << std::endl;
+ for( std::map< unsigned, bool >::iterator itw = it->second.begin(); itw != it->second.end(); ++itw ){
+ unsigned idw = itw->first;
+ if( std::find( d_update_list.begin(), d_update_list.end(), idw )==d_update_list.end() ){
+ Trace("qip-prop-debug") << "...will update " << idw << std::endl;
+ d_update_list.push_back( idw );
+ }
+ }
+ d_watch_list.erase( c );
+ }
+ }
+ }
+ }else{
+ std::vector< Node > exp_e;
+ if( d_qy.areEqualExp( a, b, exp_e ) ){
+ EqualityQueryInstProp::merge_exp( exp, exp_e );
+ conflict( exp );
+ }else{
+ //TODO?
+ }
+ }
+}
+
+void InstPropagator::conflict( std::vector< Node >& exp ) {
+ Trace("qip-propagate") << "Conflict, exp size =" << exp.size() << std::endl;
+ d_conflict = true;
+ d_relevant_inst.clear();
+ addRelevantInstances( exp, "qip-propagate" );
+}
+
+bool InstPropagator::cacheConclusion( unsigned id, Node body, int prop_index ) {
+ Assert( prop_index==0 || prop_index==1 );
+ //check if the conclusion is non-redundant
+ if( d_conc_to_id[prop_index].find( body )==d_conc_to_id[prop_index].end() ){
+ d_conc_to_id[prop_index][body] = id;
+ return true;
+ }else{
+ return false;
+ }
+}
+
+void InstPropagator::addRelevantInstances( std::vector< Node >& exp, const char * c ) {
+ for( unsigned i=0; i<exp.size(); i++ ){
+ Assert( d_conc_to_id[0].find( exp[i] )!=d_conc_to_id[0].end() );
+ Trace(c) << " relevant instance id : " << d_conc_to_id[0][ exp[i] ] << std::endl;
+ d_relevant_inst[ d_conc_to_id[0][ exp[i] ] ] = true;
+ }
+}
+
+void InstPropagator::debugPrintExplanation( std::vector< Node >& exp, const char * c ) {
+ for( unsigned i=0; i<exp.size(); i++ ){
+ Assert( d_conc_to_id[0].find( exp[i] )!=d_conc_to_id[0].end() );
+ Trace(c) << d_conc_to_id[0][ exp[i] ] << " ";
+ }
+}
+
diff --git a/src/theory/quantifiers/inst_propagator.h b/src/theory/quantifiers/inst_propagator.h new file mode 100644 index 000000000..0e21dc0d4 --- /dev/null +++ b/src/theory/quantifiers/inst_propagator.h @@ -0,0 +1,160 @@ +/********************* */
+/*! \file inst_propagator.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Propagate mechanism for instantiations
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__QUANTIFIERS_INST_PROPAGATOR_H
+#define __CVC4__QUANTIFIERS_INST_PROPAGATOR_H
+
+#include <iostream>
+#include <string>
+#include <vector>
+#include <map>
+#include "expr/node.h"
+#include "expr/type_node.h"
+#include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/term_database.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class EqualityQueryInstProp : public EqualityQuery {
+private:
+ /** pointer to quantifiers engine */
+ QuantifiersEngine* d_qe;
+public:
+ EqualityQueryInstProp( QuantifiersEngine* qe );
+ ~EqualityQueryInstProp(){};
+ /** reset */
+ bool reset( Theory::Effort e );
+ /** identify */
+ std::string identify() const { return "EqualityQueryInstProp"; }
+ /** extends engine */
+ bool extendsEngine() { return true; }
+ /** contains term */
+ bool hasTerm( Node a );
+ /** get the representative of the equivalence class of a */
+ Node getRepresentative( Node a );
+ /** returns true if a and b are equal in the current context */
+ bool areEqual( Node a, Node b );
+ /** returns true is a and b are disequal in the current context */
+ bool areDisequal( Node a, Node b );
+ /** get the equality engine associated with this query */
+ eq::EqualityEngine* getEngine();
+ /** get the equivalence class of a */
+ void getEquivalenceClass( Node a, std::vector< Node >& eqc );
+ /** get congruent term */
+ TNode getCongruentTerm( Node f, std::vector< TNode >& args );
+public:
+ /** get the representative of the equivalence class of a, with explanation */
+ Node getRepresentativeExp( Node a, std::vector< Node >& exp );
+ /** returns true if a and b are equal in the current context */
+ bool areEqualExp( Node a, Node b, std::vector< Node >& exp );
+ /** returns true is a and b are disequal in the current context */
+ bool areDisequalExp( Node a, Node b, std::vector< Node >& exp );
+private:
+ /** term index */
+ std::map< Node, TermArgTrie > d_func_map_trie;
+ /** union find for terms beyond what is stored in equality engine */
+ std::map< Node, Node > d_uf;
+ std::map< Node, std::vector< Node > > d_uf_exp;
+ Node getUfRepresentative( Node a, std::vector< Node >& exp );
+ /** disequality list, stores explanations */
+ std::map< Node, std::map< Node, Node > > d_diseq_list;
+ /** add arg */
+ void addArgument( std::vector< TNode >& args, std::vector< TNode >& props, Node n, bool is_prop, bool pol );
+public:
+ enum {
+ STATUS_MERGED_KNOWN,
+ STATUS_MERGED_UNKNOWN,
+ STATUS_NONE,
+ };
+ /** set equal */
+ int setEqual( Node& a, Node& b, std::vector< Node >& reason );
+ Node d_true;
+ Node d_false;
+public:
+ //for explanations
+ static void merge_exp( std::vector< Node >& v, std::vector< Node >& v_to_merge, int up_to_size = -1 );
+
+ Node evaluateTermExp( TNode n, std::vector< Node >& exp, std::map< TNode, Node >& visited, bool hasPol, bool pol,
+ std::map< Node, bool >& watch_list_out, std::vector< TNode >& props );
+ static bool isLiteral( Node n );
+};
+
+class InstPropagator : public QuantifiersUtil {
+private:
+ /** pointer to quantifiers engine */
+ QuantifiersEngine* d_qe;
+ /** notify class */
+ class InstantiationNotifyInstPropagator : public InstantiationNotify {
+ InstPropagator& d_ip;
+ public:
+ InstantiationNotifyInstPropagator(InstPropagator& ip): d_ip(ip) {}
+ virtual void notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) { d_ip.notifyInstantiation( quant_e, q, lem, terms, body ); }
+ };
+ InstantiationNotifyInstPropagator d_notify;
+ /** notify instantiation method */
+ void notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body );
+ /** equality query */
+ EqualityQueryInstProp d_qy;
+ class InstInfo {
+ public:
+ bool d_active;
+ Node d_q;
+ Node d_lem;
+ std::vector< Node > d_terms;
+ // the current entailed body
+ Node d_curr;
+ //explanation for current entailed body
+ std::vector< Node > d_curr_exp;
+ void init( Node q, Node lem, std::vector< Node >& terms, Node body );
+ };
+ /** instantiation count/info */
+ unsigned d_icount;
+ std::map< unsigned, InstInfo > d_ii;
+ std::map< TNode, unsigned > d_conc_to_id[2];
+ /** are we in conflict */
+ bool d_conflict;
+ /** watch list */
+ std::map< Node, std::map< unsigned, bool > > d_watch_list;
+ /** update list */
+ std::vector< unsigned > d_update_list;
+ /** relevant instances */
+ std::map< unsigned, bool > d_relevant_inst;
+private:
+ bool update( unsigned id, InstInfo& i, bool firstTime = false );
+ void propagate( Node a, Node b, bool pol, std::vector< Node >& exp );
+ void conflict( std::vector< Node >& exp );
+ bool cacheConclusion( unsigned id, Node body, int prop_index = 0 );
+ void addRelevantInstances( std::vector< Node >& exp, const char * c );
+
+ void debugPrintExplanation( std::vector< Node >& exp, const char * c );
+public:
+ InstPropagator( QuantifiersEngine* qe );
+ ~InstPropagator(){}
+ /** reset */
+ bool reset( Theory::Effort e );
+ /** identify */
+ std::string identify() const { return "InstPropagator"; }
+ /** get the notify mechanism */
+ InstantiationNotify* getInstantiationNotify() { return &d_notify; }
+};
+
+}
+}
+}
+
+#endif
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index e1cbbcfe3..e5df41510 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -1061,16 +1061,27 @@ void MatchGen::reset_round( QuantConflictFind * p ) { d_qni_gterm_rep[it->first] = p->getRepresentative( it->second ); } if( d_type==typ_ground ){ - int e = p->evaluate( d_n ); - if( e==1 ){ - d_ground_eval[0] = p->d_true; - }else if( e==-1 ){ - d_ground_eval[0] = p->d_false; + //int e = p->evaluate( d_n ); + //if( e==1 ){ + // d_ground_eval[0] = p->d_true; + //}else if( e==-1 ){ + // d_ground_eval[0] = p->d_false; + //} + //modified + for( unsigned i=0; i<2; i++ ){ + if( p->getTermDatabase()->isEntailed( d_n, i==0 ) ){ + d_ground_eval[0] = i==0 ? p->d_true : p->d_false; + } } }else if( d_type==typ_eq ){ for( unsigned i=0; i<d_n.getNumChildren(); i++ ){ if( !d_n[i].hasBoundVar() ){ - d_ground_eval[i] = p->evaluateTerm( d_n[i] ); + TNode t = p->getTermDatabase()->getEntailedTerm( d_n[i] ); + if( t.isNull() ){ + d_ground_eval[i] = d_n[i]; + }else{ + d_ground_eval[i] = t; + } } } } @@ -1103,8 +1114,12 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) { int vn = qi->getCurrentRepVar( qi->getVarNum( n ) ); if( vn==-1 ){ //evaluate the value, see if it is compatible - int e = p->evaluate( n ); - if( ( e==1 && d_tgt ) || ( e==0 && !d_tgt ) ){ + //int e = p->evaluate( n ); + //if( ( e==1 && d_tgt ) || ( e==0 && !d_tgt ) ){ + // d_child_counter = 0; + //} + //modified + if( p->getTermDatabase()->isEntailed( n, d_tgt ) ){ d_child_counter = 0; } }else{ @@ -1787,84 +1802,6 @@ void QuantConflictFind::registerQuantifier( Node q ) { } } -int QuantConflictFind::evaluate( Node n, bool pref, bool hasPref ) { - int ret = 0; - if( n.getKind()==EQUAL ){ - Node n1 = evaluateTerm( n[0] ); - Node n2 = evaluateTerm( n[1] ); - Debug("qcf-eval") << "Evaluate : Normalize " << n << " to " << n1 << " = " << n2 << std::endl; - if( areEqual( n1, n2 ) ){ - ret = 1; - }else if( areDisequal( n1, n2 ) ){ - ret = -1; - } - //else if( d_effort>QuantConflictFind::effort_conflict ){ - // ret = -1; - //} - }else if( MatchGen::isHandledUfTerm( n ) ){ //predicate - Node nn = evaluateTerm( n ); - Debug("qcf-eval") << "Evaluate : Normalize " << nn << " to " << n << std::endl; - if( areEqual( nn, d_true ) ){ - ret = 1; - }else if( areEqual( nn, d_false ) ){ - ret = -1; - } - //else if( d_effort>QuantConflictFind::effort_conflict ){ - // ret = -1; - //} - }else if( n.getKind()==NOT ){ - return -evaluate( n[0] ); - }else if( n.getKind()==ITE ){ - int cev1 = evaluate( n[0] ); - int cevc[2] = { 0, 0 }; - for( unsigned i=0; i<2; i++ ){ - if( ( i==0 && cev1!=-1 ) || ( i==1 && cev1!=1 ) ){ - cevc[i] = evaluate( n[i+1] ); - if( cev1!=0 ){ - ret = cevc[i]; - break; - }else if( cevc[i]==0 ){ - break; - } - } - } - if( ret==0 && cevc[0]!=0 && cevc[0]==cevc[1] ){ - ret = cevc[0]; - } - }else if( n.getKind()==IFF ){ - int cev1 = evaluate( n[0] ); - if( cev1!=0 ){ - int cev2 = evaluate( n[1] ); - if( cev2!=0 ){ - ret = cev1==cev2 ? 1 : -1; - } - } - - }else{ - int ssval = 0; - if( n.getKind()==OR ){ - ssval = 1; - }else if( n.getKind()==AND ){ - ssval = -1; - } - bool isUnk = false; - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - int cev = evaluate( n[i] ); - if( cev==ssval ){ - ret = ssval; - break; - }else if( cev==0 ){ - isUnk = true; - } - } - if( ret==0 && !isUnk ){ - ret = -ssval; - } - } - Debug("qcf-eval") << "Evaluate " << n << " to " << ret << std::endl; - return ret; -} - short QuantConflictFind::getMaxQcfEffort() { if( options::qcfMode()==QCF_CONFLICT_ONLY ){ return effort_conflict; @@ -1908,38 +1845,6 @@ void QuantConflictFind::assertNode( Node q ) { } } -Node QuantConflictFind::evaluateTerm( Node n ) { - if( MatchGen::isHandledUfTerm( n ) ){ - Node f = MatchGen::getMatchOperator( this, n ); - Node nn; - if( getEqualityEngine()->hasTerm( n ) ){ - nn = getTermDatabase()->existsTerm( f, n ); - }else{ - std::vector< TNode > args; - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - Node c = evaluateTerm( n[i] ); - args.push_back( c ); - } - nn = getTermDatabase()->d_func_map_trie[f].existsTerm( args ); - } - if( !nn.isNull() ){ - Debug("qcf-eval") << "GT: Term " << nn << " for " << n << " hasTerm = " << getEqualityEngine()->hasTerm( n ) << std::endl; - return getRepresentative( nn ); - }else{ - Debug("qcf-eval") << "GT: No term for " << n << " hasTerm = " << getEqualityEngine()->hasTerm( n ) << std::endl; - return n; - } - }else if( n.getKind()==ITE ){ - int v = evaluate( n[0], false, false ); - if( v==1 ){ - return evaluateTerm( n[1] ); - }else if( v==-1 ){ - return evaluateTerm( n[2] ); - } - } - return getRepresentative( n ); -} - /** new node */ void QuantConflictFind::newEqClass( Node n ) { @@ -2055,13 +1960,12 @@ void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) { std::vector< Node > terms; qi->getMatch( terms ); if( !qi->isTConstraintSpurious( this, terms ) ){ + //for debugging if( Debug.isOn("qcf-check-inst") ){ - //if( e==effort_conflict ){ Node inst = d_quantEngine->getInstantiation( q, terms ); Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl; - Assert( evaluate( inst )!=1 ); - Assert( evaluate( inst )==-1 || e>effort_conflict ); - //} + Assert( !getTermDatabase()->isEntailed( inst, true ) ); + Assert( getTermDatabase()->isEntailed( inst, false ) || e>effort_conflict ); } if( d_quantEngine->addInstantiation( q, terms, false ) ){ Trace("qcf-check") << " ... Added instantiation" << std::endl; diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 0e0e78100..36fcaddf5 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -192,9 +192,6 @@ public: //for ground terms Node d_false; TNode getZero( Kind k ); private: - Node evaluateTerm( Node n ); - int evaluate( Node n, bool pref = false, bool hasPref = false ); -private: //currently asserted quantifiers NodeList d_qassert; std::map< Node, QuantInfo > d_qinfo; diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index 5fbc46954..3b7787a20 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -23,6 +23,38 @@ using namespace CVC4::kind; using namespace CVC4::context; using namespace CVC4::theory; + +unsigned QuantifiersModule::needsModel( Theory::Effort e ) { + return QuantifiersEngine::QEFFORT_NONE; +} + +eq::EqualityEngine * QuantifiersModule::getEqualityEngine() { + return d_quantEngine->getMasterEqualityEngine(); +} + +bool QuantifiersModule::areEqual( TNode n1, TNode n2 ) { + eq::EqualityEngine * ee = getEqualityEngine(); + return n1==n2 || ( ee->hasTerm( n1 ) && ee->hasTerm( n2 ) && ee->areEqual( n1, n2 ) ); +} + +bool QuantifiersModule::areDisequal( TNode n1, TNode n2 ) { + eq::EqualityEngine * ee = getEqualityEngine(); + return n1!=n2 && ee->hasTerm( n1 ) && ee->hasTerm( n2 ) && ee->areDisequal( n1, n2, false ); +} + +TNode QuantifiersModule::getRepresentative( TNode n ) { + eq::EqualityEngine * ee = getEqualityEngine(); + if( ee->hasTerm( n ) ){ + return ee->getRepresentative( n ); + }else{ + return n; + } +} + +quantifiers::TermDb * QuantifiersModule::getTermDatabase() { + return d_quantEngine->getTermDatabase(); +} + bool QuantArith::getMonomial( Node n, Node& c, Node& v ){ if( n.getKind()==MULT && n.getNumChildren()==2 && n[0].isConst() ){ c = n[0]; diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 8db79db9c..79cdae437 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -29,6 +29,58 @@ namespace theory { class QuantifiersEngine; +namespace quantifiers { + class TermDb; +} + +class QuantifiersModule { +protected: + QuantifiersEngine* d_quantEngine; +public: + QuantifiersModule( QuantifiersEngine* qe ) : d_quantEngine( qe ){} + virtual ~QuantifiersModule(){} + //get quantifiers engine + QuantifiersEngine* getQuantifiersEngine() { return d_quantEngine; } + /** presolve */ + virtual void presolve() {} + /* whether this module needs to check this round */ + virtual bool needsCheck( Theory::Effort e ) { return e>=Theory::EFFORT_LAST_CALL; } + /* whether this module needs a model built */ + virtual unsigned needsModel( Theory::Effort e ); + /* reset at a round */ + virtual void reset_round( Theory::Effort e ){} + /* Call during quantifier engine's check */ + virtual void check( Theory::Effort e, unsigned quant_e ) = 0; + /* check was complete (e.g. no lemmas implies a model) */ + virtual bool checkComplete() { return true; } + /* Called for new quantified formulas */ + virtual void preRegisterQuantifier( Node q ) { } + /* Called for new quantifiers after owners are finalized */ + virtual void registerQuantifier( Node q ) = 0; + virtual void assertNode( Node n ) {} + virtual void propagate( Theory::Effort level ){} + virtual Node getNextDecisionRequest() { return TNode::null(); } + /** Identify this module (for debugging, dynamic configuration, etc..) */ + virtual std::string identify() const = 0; +public: + eq::EqualityEngine * getEqualityEngine(); + bool areDisequal( TNode n1, TNode n2 ); + bool areEqual( TNode n1, TNode n2 ); + TNode getRepresentative( TNode n ); + quantifiers::TermDb * getTermDatabase(); +};/* class QuantifiersModule */ + +class QuantifiersUtil { +public: + QuantifiersUtil(){} + virtual ~QuantifiersUtil(){} + /* reset at a round */ + virtual bool reset( Theory::Effort e ) = 0; + /** Identify this module (for debugging, dynamic configuration, etc..) */ + virtual std::string identify() const = 0; +}; + + class QuantArith { public: @@ -97,7 +149,7 @@ public: }; -class EqualityQuery { +class EqualityQuery : public QuantifiersUtil{ public: EqualityQuery(){} virtual ~EqualityQuery(){}; @@ -115,6 +167,8 @@ public: virtual eq::EqualityEngine* getEngine() = 0; /** get the equivalence class of a */ virtual void getEquivalenceClass( Node a, std::vector< Node >& eqc ) = 0; + /** get the term that exists in EE that is congruent to f with args (f is returned by TermDb::getMatchOperator(...) */ + virtual TNode getCongruentTerm( Node f, std::vector< TNode >& args ) = 0; };/* class EqualityQuery */ diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index 6cc14c023..9181677ee 100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -82,8 +82,9 @@ RelevantDomain::RDomain * RelevantDomain::getRDomain( Node n, int i, bool getPar return getParent ? d_rel_doms[n][i]->getParent() : d_rel_doms[n][i]; } -void RelevantDomain::reset(){ +bool RelevantDomain::reset( Theory::Effort e ) { d_is_computed = false; + return true; } void RelevantDomain::compute(){ diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h index 819e0e7b6..2b90520fd 100644 --- a/src/theory/quantifiers/relevant_domain.h +++ b/src/theory/quantifiers/relevant_domain.h @@ -23,7 +23,7 @@ namespace CVC4 { namespace theory { namespace quantifiers { -class RelevantDomain +class RelevantDomain : public QuantifiersUtil { private: class RDomain @@ -62,7 +62,10 @@ private: public: RelevantDomain( QuantifiersEngine* qe, FirstOrderModel* m ); virtual ~RelevantDomain(){} - void reset(); + /* reset */ + bool reset( Theory::Effort e ); + /** identify */ + std::string identify() const { return "RelevantDomain"; } //compute the relevant domain void compute(); diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 763a80af3..3d3646d7d 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -205,67 +205,59 @@ void TermDb::computeUfEqcTerms( TNode f ) { } } -//returns a term n' equivalent to n -// - if hasSubs = true, then n is consider under substitution subs -// - if mkNewTerms = true, then n' is either null, or a term in the master equality engine -Node TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, std::map< TNode, Node >& visited, EqualityQuery * qy ) { +//return a term n' equivalent to n +// maximal subterms of n' are representatives in the equality engine qy +Node TermDb::evaluateTerm2( TNode n, std::map< TNode, Node >& visited, EqualityQuery * qy ) { std::map< TNode, Node >::iterator itv = visited.find( n ); if( itv != visited.end() ){ return itv->second; } - Node ret; + Assert( n.getKind()!=BOUND_VARIABLE ); Trace("term-db-eval") << "evaluate term : " << n << std::endl; - if( qy->hasTerm( n ) ){ - Trace("term-db-eval") << "...exists in ee, return rep " << std::endl; - ret = qy->getRepresentative( n ); - }else if( n.getKind()==BOUND_VARIABLE ){ - if( hasSubs ){ - Assert( subs.find( n )!=subs.end() ); - Trace("term-db-eval") << "...substitution is : " << subs[n] << std::endl; - if( subsRep ){ - Assert( qy->hasTerm( subs[n] ) ); - Assert( qy->getRepresentative( subs[n] )==subs[n] ); - ret = subs[n]; - }else{ - ret = evaluateTerm2( subs[n], subs, subsRep, hasSubs, visited, qy ); - } - } - }else if( n.getKind()==FORALL ){ - ret = n; - }else{ - if( n.hasOperator() ){ + Node ret; + if( !qy->hasTerm( n ) ){ + //term is not known to be equal to a representative in equality engine, evaluate it + if( n.getKind()==FORALL ){ + ret = Node::null(); + }else if( n.hasOperator() ){ TNode f = getMatchOperator( n ); std::vector< TNode > args; bool ret_set = false; for( unsigned i=0; i<n.getNumChildren(); i++ ){ - TNode c = evaluateTerm2( n[i], subs, subsRep, hasSubs, visited, qy ); + TNode c = evaluateTerm2( n[i], visited, qy ); if( c.isNull() ){ - ret = TNode::null(); + ret = Node::null(); ret_set = true; break; + }else if( c==d_true || c==d_false ){ + //short-circuiting + if( ( n.getKind()==kind::AND && c==d_false ) || ( n.getKind()==kind::OR && c==d_true ) ){ + ret = c; + ret_set = true; + break; + }else if( n.getKind()==kind::ITE && i==0 ){ + ret = evaluateTerm2( n[ c==d_true ? 1 : 2], visited, qy ); + ret_set = true; + break; + } } - Trace("term-db-eval") << "Child " << i << " : " << c << std::endl; - //short-circuit and/or - if( ( n.getKind()==kind::AND && c==d_false ) || ( n.getKind()==kind::OR && c==d_true ) ){ - ret = c; - ret_set = true; - break; - }else{ - args.push_back( c ); - } + Trace("term-db-eval") << " child " << i << " : " << c << std::endl; + args.push_back( c ); } if( !ret_set ){ + //if it is an indexed term, return the congruent term if( !f.isNull() ){ - Trace("term-db-eval") << "Get term from DB" << std::endl; - TNode nn = d_func_map_trie[f].existsTerm( args ); - Trace("term-db-eval") << "Got term " << nn << std::endl; - if( !nn.isNull() && qy->hasTerm( nn ) ){ - Trace("term-db-eval") << "return rep " << std::endl; + TNode nn = qy->getCongruentTerm( f, args ); + Trace("term-db-eval") << " got congruent term " << nn << " from DB for " << n << std::endl; + if( !nn.isNull() ){ ret = qy->getRepresentative( nn ); + Trace("term-db-eval") << "return rep" << std::endl; ret_set = true; + Assert( !ret.isNull() ); } } if( !ret_set ){ + Trace("term-db-eval") << "return rewrite" << std::endl; //a theory symbol or a new UF term if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ args.insert( args.begin(), n.getOperator() ); @@ -275,6 +267,9 @@ Node TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRe } } } + }else{ + Trace("term-db-eval") << "...exists in ee, return rep" << std::endl; + ret = qy->getRepresentative( n ); } Trace("term-db-eval") << "evaluated term : " << n << ", got : " << ret << std::endl; visited[n] = ret; @@ -282,22 +277,28 @@ Node TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRe } -TNode TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy ) { +TNode TermDb::getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy ) { Assert( !qy->extendsEngine() ); - Trace("term-db-eval") << "evaluate term : " << n << std::endl; + Trace("term-db-entail") << "get entailed term : " << n << std::endl; if( qy->getEngine()->hasTerm( n ) ){ - Trace("term-db-eval") << "...exists in ee, return rep " << std::endl; + Trace("term-db-entail") << "...exists in ee, return rep " << std::endl; return n; }else if( n.getKind()==BOUND_VARIABLE ){ if( hasSubs ){ Assert( subs.find( n )!=subs.end() ); - Trace("term-db-eval") << "...substitution is : " << subs[n] << std::endl; + Trace("term-db-entail") << "...substitution is : " << subs[n] << std::endl; if( subsRep ){ Assert( qy->getEngine()->hasTerm( subs[n] ) ); Assert( qy->getEngine()->getRepresentative( subs[n] )==subs[n] ); return subs[n]; }else{ - return evaluateTerm2( subs[n], subs, subsRep, hasSubs, qy ); + return getEntailedTerm2( subs[n], subs, subsRep, hasSubs, qy ); + } + } + }else if( n.getKind()==ITE ){ + for( unsigned i=0; i<2; i++ ){ + if( isEntailed2( n[0], subs, subsRep, hasSubs, i==0, qy ) ){ + return getEntailedTerm2( n[ i==0 ? 1 : 2 ], subs, subsRep, hasSubs, qy ); } } }else{ @@ -306,17 +307,16 @@ TNode TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsR if( !f.isNull() ){ std::vector< TNode > args; for( unsigned i=0; i<n.getNumChildren(); i++ ){ - TNode c = evaluateTerm2( n[i], subs, subsRep, hasSubs, qy ); + TNode c = getEntailedTerm2( n[i], subs, subsRep, hasSubs, qy ); if( c.isNull() ){ return TNode::null(); } c = qy->getEngine()->getRepresentative( c ); - Trace("term-db-eval") << "Got child : " << c << std::endl; + Trace("term-db-entail") << " child " << i << " : " << c << std::endl; args.push_back( c ); } - Trace("term-db-eval") << "Get term from DB" << std::endl; - TNode nn = d_func_map_trie[f].existsTerm( args ); - Trace("term-db-eval") << "Got term " << nn << std::endl; + TNode nn = qy->getCongruentTerm( f, args ); + Trace("term-db-entail") << " got congruent term " << nn << " for " << n << std::endl; return nn; } } @@ -324,39 +324,37 @@ TNode TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsR return TNode::null(); } -Node TermDb::evaluateTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool mkNewTerms, EqualityQuery * qy ) { +Node TermDb::evaluateTerm( TNode n, EqualityQuery * qy ) { if( qy==NULL ){ qy = d_quantEngine->getEqualityQuery(); } - if( mkNewTerms ){ - std::map< TNode, Node > visited; - return evaluateTerm2( n, subs, subsRep, true, visited, qy ); - }else{ - return evaluateTerm2( n, subs, subsRep, true, qy ); + std::map< TNode, Node > visited; + return evaluateTerm2( n, visited, qy ); +} + +TNode TermDb::getEntailedTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep, EqualityQuery * qy ) { + if( qy==NULL ){ + qy = d_quantEngine->getEqualityQuery(); } + return getEntailedTerm2( n, subs, subsRep, true, qy ); } -Node TermDb::evaluateTerm( TNode n, bool mkNewTerms, EqualityQuery * qy ) { +TNode TermDb::getEntailedTerm( TNode n, EqualityQuery * qy ) { if( qy==NULL ){ qy = d_quantEngine->getEqualityQuery(); } std::map< TNode, TNode > subs; - if( mkNewTerms ){ - std::map< TNode, Node > visited; - return evaluateTerm2( n, subs, false, false, visited, qy ); - }else{ - return evaluateTerm2( n, subs, false, false, qy ); - } + return getEntailedTerm2( n, subs, false, false, qy ); } -bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol, EqualityQuery * qy ) { +bool TermDb::isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol, EqualityQuery * qy ) { Assert( !qy->extendsEngine() ); - Trace("term-db-eval") << "Check entailed : " << n << ", pol = " << pol << std::endl; + Trace("term-db-entail") << "Check entailed : " << n << ", pol = " << pol << std::endl; Assert( n.getType().isBoolean() ); if( n.getKind()==EQUAL ){ - TNode n1 = evaluateTerm2( n[0], subs, subsRep, hasSubs, qy ); + TNode n1 = getEntailedTerm2( n[0], subs, subsRep, hasSubs, qy ); if( !n1.isNull() ){ - TNode n2 = evaluateTerm2( n[1], subs, subsRep, hasSubs, qy ); + TNode n2 = getEntailedTerm2( n[1], subs, subsRep, hasSubs, qy ); if( !n2.isNull() ){ if( n1==n2 ){ return pol; @@ -372,11 +370,11 @@ bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, } } }else if( n.getKind()==NOT ){ - return isEntailed( n[0], subs, subsRep, hasSubs, !pol, qy ); + return isEntailed2( n[0], subs, subsRep, hasSubs, !pol, qy ); }else if( n.getKind()==OR || n.getKind()==AND ){ bool simPol = ( pol && n.getKind()==OR ) || ( !pol && n.getKind()==AND ); for( unsigned i=0; i<n.getNumChildren(); i++ ){ - if( isEntailed( n[i], subs, subsRep, hasSubs, pol, qy ) ){ + if( isEntailed2( n[i], subs, subsRep, hasSubs, pol, qy ) ){ if( simPol ){ return true; } @@ -389,14 +387,14 @@ bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, return !simPol; }else if( n.getKind()==IFF || n.getKind()==ITE ){ for( unsigned i=0; i<2; i++ ){ - if( isEntailed( n[0], subs, subsRep, hasSubs, i==0, qy ) ){ + if( isEntailed2( n[0], subs, subsRep, hasSubs, i==0, qy ) ){ unsigned ch = ( n.getKind()==IFF || i==0 ) ? 1 : 2; bool reqPol = ( n.getKind()==ITE || i==0 ) ? pol : !pol; - return isEntailed( n[ch], subs, subsRep, hasSubs, reqPol, qy ); + return isEntailed2( n[ch], subs, subsRep, hasSubs, reqPol, qy ); } } }else if( n.getKind()==APPLY_UF ){ - TNode n1 = evaluateTerm2( n, subs, subsRep, hasSubs, qy ); + TNode n1 = getEntailedTerm2( n, subs, subsRep, hasSubs, qy ); if( !n1.isNull() ){ Assert( qy->hasTerm( n1 ) ); if( n1==d_true ){ @@ -411,16 +409,21 @@ bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, return false; } -bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol, EqualityQuery * qy ) { +bool TermDb::isEntailed( TNode n, bool pol, EqualityQuery * qy ) { if( qy==NULL ){ + Assert( d_consistent_ee ); qy = d_quantEngine->getEqualityQuery(); } - if( d_consistent_ee ){ - return isEntailed( n, subs, subsRep, true, pol, qy ); - }else{ - //don't check entailment wrt an inconsistent ee - return false; + std::map< TNode, TNode > subs; + return isEntailed2( n, subs, false, false, pol, qy ); +} + +bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol, EqualityQuery * qy ) { + if( qy==NULL ){ + Assert( d_consistent_ee ); + qy = d_quantEngine->getEqualityQuery(); } + return isEntailed2( n, subs, subsRep, true, pol, qy ); } bool TermDb::hasTermCurrent( Node n, bool useMode ) { @@ -571,7 +574,13 @@ bool TermDb::reset( Theory::Effort effort ){ } } } - + //explicitly add inst closure terms to the equality engine to ensure only EE terms are indexed + for( std::hash_set< Node, NodeHashFunction >::iterator it = d_iclosure_processed.begin(); it !=d_iclosure_processed.end(); ++it ){ + Node n = *it; + if( !ee->hasTerm( n ) ){ + ee->addTerm( n ); + } + } //rebuild d_func/pred_map_trie for each operation, this will calculate all congruent terms for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){ @@ -579,8 +588,8 @@ bool TermDb::reset( Theory::Effort effort ){ Trace("term-db-debug") << "Adding terms for operator " << it->first << std::endl; for( unsigned i=0; i<it->second.size(); i++ ){ Node n = it->second[i]; - //to be added to term index, term must be relevant, and either exist in EE or be an inst closure term - if( hasTermCurrent( n ) && ( ee->hasTerm( n ) || d_iclosure_processed.find( n )!=d_iclosure_processed.end() ) ){ + //to be added to term index, term must be relevant, and exist in EE + if( hasTermCurrent( n ) && ee->hasTerm( n ) ){ if( !n.getAttribute(NoMatchAttribute()) ){ if( options::finiteModelFind() ){ computeModelBasisArgAttribute( n ); @@ -681,11 +690,15 @@ TermArgTrie * TermDb::getTermArgTrie( Node eqc, Node f ) { } } -TNode TermDb::existsTerm( Node f, Node n ) { +TNode TermDb::getCongruentTerm( Node f, Node n ) { computeArgReps( n ); return d_func_map_trie[f].existsTerm( d_arg_reps[n] ); } +TNode TermDb::getCongruentTerm( Node f, std::vector< TNode >& args ) { + return d_func_map_trie[f].existsTerm( args ); +} + Node TermDb::getModelBasisTerm( TypeNode tn, int i ){ if( d_model_basis_term.find( tn )==d_model_basis_term.end() ){ Node mbt; diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 9177d3a1a..76bd623a8 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -164,7 +164,7 @@ namespace fmcheck { class TermDbSygus; -class TermDb { +class TermDb : public QuantifiersUtil { friend class ::CVC4::theory::QuantifiersEngine; friend class ::CVC4::theory::inst::Trigger; friend class ::CVC4::theory::quantifiers::fmcheck::FullModelChecker; @@ -183,9 +183,9 @@ private: /** set has term */ void setHasTerm( Node n ); /** evaluate term */ - TNode evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy ); - Node evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, std::map< TNode, Node >& visited, EqualityQuery * qy ); - bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol, EqualityQuery * qy ); + Node evaluateTerm2( TNode n, std::map< TNode, Node >& visited, EqualityQuery * qy ); + TNode getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy ); + bool isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol, EqualityQuery * qy ); public: TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ); ~TermDb(){} @@ -224,13 +224,16 @@ public: void presolve(); /** reset (calculate which terms are active) */ bool reset( Theory::Effort effort ); + /** identify */ + std::string identify() const { return "TermDb"; } /** get match operator */ Node getMatchOperator( Node n ); /** get term arg index */ TermArgTrie * getTermArgTrie( Node f ); TermArgTrie * getTermArgTrie( Node eqc, Node f ); /** exists term */ - TNode existsTerm( Node f, Node n ); + TNode getCongruentTerm( Node f, Node n ); + TNode getCongruentTerm( Node f, std::vector< TNode >& args ); /** compute arg reps */ void computeArgReps( TNode n ); /** compute uf eqc terms */ @@ -238,10 +241,12 @@ public: /** evaluate a term under a substitution. Return representative in EE if possible. * subsRep is whether subs contains only representatives */ - Node evaluateTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool mkNewTerms = false, EqualityQuery * qy = NULL ); - /** same as above, but without substitution */ - Node evaluateTerm( TNode n, bool mkNewTerms = false, EqualityQuery * qy = NULL ); + Node evaluateTerm( TNode n, EqualityQuery * qy = NULL ); + /** get entailed term, does not construct new terms, less aggressive */ + TNode getEntailedTerm( TNode n, EqualityQuery * qy = NULL ); + TNode getEntailedTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep, EqualityQuery * qy = NULL ); /** is entailed (incomplete check) */ + bool isEntailed( TNode n, bool pol, EqualityQuery * qy = NULL ); bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol, EqualityQuery * qy = NULL ); /** has term */ bool hasTermCurrent( Node n, bool useMode = true ); |