theory/quantifiers/quant_split.cpp \
theory/quantifiers/anti_skolem.h \
theory/quantifiers/anti_skolem.cpp \
+ theory/quantifiers/equality_infer.h \
+ theory/quantifiers/equality_infer.cpp \
theory/arith/theory_arith_type_rules.h \
theory/arith/type_enumerator.h \
theory/arith/arithvar.h \
--- /dev/null
+/********************* */
+/*! \file equality_infer.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
+ **
+ ** \brief Method for inferring equalities between arithmetic equivalence classes,
+ ** inspired by "A generalization of Shostak's method for combining decision procedures" Barrett et al. Figure 1.
+ **
+ **/
+
+#include "theory/quantifiers/equality_infer.h"
+#include "theory/quantifiers/quant_util.h"
+#include "context/context_mm.h"
+
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+using namespace std;
+
+namespace CVC4 {
+
+EqualityInference::EqcInfo::EqcInfo(context::Context* c) : d_rep( c ), d_valid( c, false ) {
+
+}
+
+EqualityInference::EqualityInference( context::Context* c ) : d_c( c ), d_elim_vars( c ), d_rep_to_eqc( c ), d_uselist( c ), d_pending_merges( c ){
+ d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
+}
+
+EqualityInference::~EqualityInference(){
+ for( std::map< Node, EqcInfo * >::iterator it = d_eqci.begin(); it != d_eqci.end(); ++it ){
+ delete it->second;
+ }
+}
+
+void EqualityInference::eqNotifyNewClass(TNode t) {
+ if( t.getType().isReal() ){
+ Trace("eq-infer") << "Notify equivalence class : " << t << std::endl;
+ EqcInfo * eqci;
+ std::map< Node, EqcInfo * >::iterator itec = d_eqci.find( t );
+ if( itec==d_eqci.end() ){
+ eqci = new EqcInfo( d_c );
+ d_eqci[t] = eqci;
+ }else{
+ eqci = itec->second;
+ }
+ std::map< Node, Node > msum;
+ if( QuantArith::getMonomialSum( t, msum ) ){
+ eqci->d_valid = true;
+ bool changed = false;
+ std::vector< Node > children;
+ for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ) {
+ Node n = it->first;
+ if( !n.isNull() ){
+ NodeMap::const_iterator itv = d_elim_vars.find( n );
+ if( itv!=d_elim_vars.end() ){
+ changed = true;
+ n = (*itv).second;
+ }
+ if( it->second.isNull() ){
+ children.push_back( n );
+ }else{
+ children.push_back( NodeManager::currentNM()->mkNode( MULT, it->second, n ) );
+ }
+ }else{
+ children.push_back( it->second );
+ }
+ }
+ Node r;
+ bool mvalid = true;
+ if( changed ){
+ r = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( PLUS, children );
+ r = Rewriter::rewrite( r );
+ msum.clear();
+ if( !QuantArith::getMonomialSum( r, msum ) ){
+ mvalid = false;
+ }
+ }else{
+ r = t;
+ }
+ Trace("eq-infer") << "...value is " << r << std::endl;
+ setEqcRep( t, r, eqci );
+ if( mvalid ){
+ for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
+ if( !it->first.isNull() ){
+ addToUseList( it->first, t );
+ }
+ }
+ }
+ }else{
+ eqci->d_valid = false;
+ }
+ }
+}
+
+void EqualityInference::addToUseList( Node used, Node eqc ) {
+ NodeListMap::iterator ul_i = d_uselist.find( used );
+ NodeList* ul;
+ if( ul_i != d_uselist.end() ){
+ ul = (*ul_i).second;
+ }else{
+ ul = new(d_c->getCMM()) NodeList( true, d_c, false, context::ContextMemoryAllocator<TNode>(d_c->getCMM()) );
+ d_uselist.insertDataFromContextMemory( used, ul );
+ }
+ Trace("eq-infer-debug") << " add to use list : " << used << " -> " << eqc << std::endl;
+ (*ul).push_back( eqc );
+}
+
+void EqualityInference::setEqcRep( Node t, Node r, EqcInfo * eqci ) {
+ eqci->d_rep = r;
+ NodeMap::const_iterator itr = d_rep_to_eqc.find( r );
+ if( itr==d_rep_to_eqc.end() ){
+ d_rep_to_eqc[r] = t;
+ }else{
+ //merge two equivalence classes
+ Node t2 = (*itr).second;
+ //check if it is valid
+ std::map< Node, EqcInfo * >::iterator itc = d_eqci.find( t2 );
+ if( itc!=d_eqci.end() && itc->second->d_valid ){
+ Trace("eq-infer") << "Infer two equivalence classes are equal : " << t << " " << t2 << std::endl;
+ Trace("eq-infer") << " since they both normalize to : " << r << std::endl;
+ d_pending_merges.push_back( t.eqNode( t2 ) );
+ }
+ }
+}
+
+void EqualityInference::eqNotifyMerge(TNode t1, TNode t2) {
+ Assert( !t1.isNull() );
+ Assert( !t2.isNull() );
+ std::map< Node, EqcInfo * >::iterator itv1 = d_eqci.find( t1 );
+ if( itv1!=d_eqci.end() ){
+ std::map< Node, EqcInfo * >::iterator itv2 = d_eqci.find( t2 );
+ if( itv2!=d_eqci.end() ){
+ Trace("eq-infer") << "Merge equivalence classes : " << t2 << " into " << t1 << std::endl;
+ Node tr1 = itv1->second->d_rep;
+ Node tr2 = itv2->second->d_rep;
+ itv2->second->d_valid = false;
+ Trace("eq-infer") << "Representatives : " << tr2 << " into " << tr1 << std::endl;
+ if( tr1!=tr2 ){
+ Node eq = tr1.eqNode( tr2 );
+ std::map< Node, Node > msum;
+ if( QuantArith::getMonomialSumLit( eq, msum ) ){
+ Node v_solve;
+ //solve for variables with no coefficient
+ for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ) {
+ Node n = it->first;
+ if( !n.isNull() && it->second.isNull() ){
+ v_solve = n;
+ break;
+ }
+ }
+ if( !v_solve.isNull() ){
+ //solve for v_solve
+ Node veq;
+ if( QuantArith::isolate( v_solve, msum, veq, kind::EQUAL, true )==1 ){
+ Node v_value = veq[1];
+ Trace("eq-infer") << "...solved " << v_solve << " == " << v_value << std::endl;
+ Assert( d_elim_vars.find( v_solve )==d_elim_vars.end() );
+ d_elim_vars[v_solve] = v_value;
+
+ std::vector< Node > new_use;
+ for( std::map< Node, Node >::iterator itmm = msum.begin(); itmm != msum.end(); ++itmm ){
+ Node n = itmm->first;
+ if( !n.isNull() && n!=v_solve ){
+ new_use.push_back( n );
+ }
+ }
+
+ //go through all equivalence classes that may refer to v_solve
+ std::map< Node, bool > processed;
+ NodeListMap::iterator ul_i = d_uselist.find( v_solve );
+ if( ul_i != d_uselist.end() ){
+ NodeList* ul = (*ul_i).second;
+ Trace("eq-infer-debug") << " use list size = " << ul->size() << std::endl;
+ for( unsigned j=0; j<ul->size(); j++ ){
+ Node r = (*ul)[j];
+ if( processed.find( r )==processed.end() ){
+ processed[r] = true;
+ std::map< Node, EqcInfo * >::iterator itt = d_eqci.find( r );
+ if( itt!=d_eqci.end() && itt->second->d_valid ){
+ std::map< Node, Node > msum2;
+ if( QuantArith::getMonomialSum( itt->second->d_rep.get(), msum2 ) ){
+ std::map< Node, Node >::iterator itm = msum2.find( v_solve );
+ if( itm!=msum2.end() ){
+ //substitute in solved form
+ std::map< Node, Node >::iterator itm2 = msum2.find( v_value );
+ if( itm2 == msum2.end() ){
+ msum2[v_value] = itm->second;
+ }else{
+ msum2[v_value] = NodeManager::currentNM()->mkNode( PLUS, itm2->second.isNull() ? d_one : itm2->second,
+ itm->second.isNull() ? d_one : itm->second );
+ }
+ msum2.erase( itm );
+ Node rr = QuantArith::mkNode( msum2 );
+ rr = Rewriter::rewrite( rr );
+ Trace("eq-infer") << "......update " << itt->first << " => " << rr << std::endl;
+ setEqcRep( itt->first, rr, itt->second );
+ //update use list
+ for( unsigned i=0; i<new_use.size(); i++ ){
+ addToUseList( new_use[i], r );
+ }
+ }
+ }else{
+ itt->second->d_valid = false;
+ }
+ }
+ }
+ }
+ }
+ Trace("eq-infer") << "...finished solved." << std::endl;
+ }
+ }
+ }
+ }
+ }else{
+ //no information to merge
+ }
+ }else{
+ //carry information (this might happen for non-linear t1 and linear t2?)
+ std::map< Node, EqcInfo * >::iterator itv2 = d_eqci.find( t2 );
+ if( itv2!=d_eqci.end() ){
+ d_eqci[t1] = d_eqci[t2];
+ d_eqci[t2] = NULL;
+ }
+ }
+}
+
+}
--- /dev/null
+/********************* */
+/*! \file equality_infer.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 additional inference for equalities
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef EQUALITY_INFER_H
+#define EQUALITY_INFER_H
+
+#include <ext/hash_set>
+#include <iostream>
+#include <map>
+#include <vector>
+
+#include "context/context.h"
+#include "context/context_mm.h"
+#include "context/cdhashmap.h"
+#include "context/cdchunk_list.h"
+#include "context/cdhashset.h"
+#include "theory/theory.h"
+
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class EqualityInference
+{
+ typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap;
+ typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
+ typedef context::CDChunkList<Node> NodeList;
+ typedef context::CDHashMap< Node, NodeList *, NodeHashFunction > NodeListMap;
+private:
+ context::Context * d_c;
+ Node d_one;
+ class EqcInfo {
+ public:
+ EqcInfo(context::Context* c);
+ ~EqcInfo(){}
+ context::CDO< Node > d_rep;
+ context::CDO< bool > d_valid;
+ };
+
+ /** information necessary for equivalence classes */
+ NodeMap d_elim_vars;
+ std::map< Node, EqcInfo * > d_eqci;
+ NodeMap d_rep_to_eqc;
+ /** set eqc rep */
+ void setEqcRep( Node t, Node r, EqcInfo * eqci );
+ /** use list */
+ NodeListMap d_uselist;
+ void addToUseList( Node used, Node eqc );
+public:
+ EqualityInference(context::Context* c);
+ virtual ~EqualityInference();
+ /** notification when equality engine is updated */
+ void eqNotifyNewClass(TNode t);
+ void eqNotifyMerge(TNode t1, TNode t2);
+
+ NodeList d_pending_merges;
+};
+
+}
+}
+}
+
+#endif
}
}
bool QuantArith::getMonomial( Node n, std::map< Node, Node >& msum ) {
- if ( n.getKind()==MULT ){
- if( n.getNumChildren()==2 && msum.find(n[1])==msum.end() && n[0].isConst() ){
+ if( n.getKind()==MULT && n.getNumChildren()==2 && n[0].isConst() ){
+ if( msum.find(n[1])==msum.end() ){
msum[n[1]] = n[0];
return true;
}
+ }else if( n.isConst() ){
+ if( msum.find(Node::null())==msum.end() ){
+ msum[Node::null()] = n;
+ return true;
+ }
}else{
if( msum.find(n)==msum.end() ){
msum[n] = Node::null();
bool QuantArith::getMonomialSumLit( Node lit, std::map< Node, Node >& msum ) {
if( lit.getKind()==GEQ || lit.getKind()==EQUAL ){
if( getMonomialSum( lit[0], msum ) ){
- if( lit[1].isConst() ){
- if( !lit[1].getConst<Rational>().isZero() ){
- msum[Node::null()] = negate( lit[1] );
- }
+ if( lit[1].isConst() && lit[1].getConst<Rational>().isZero() ){
return true;
}else{
//subtract the other side
return false;
}
+Node QuantArith::mkNode( std::map< Node, Node >& msum ) {
+ std::vector< Node > children;
+ for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
+ Node m;
+ if( !it->first.isNull() ){
+ if( !it->second.isNull() ){
+ m = NodeManager::currentNM()->mkNode( MULT, it->second, it->first );
+ }else{
+ m = it->first;
+ }
+ }else{
+ Assert( !it->second.isNull() );
+ m = it->second;
+ }
+ children.push_back(m);
+ }
+ return children.size()>1 ? NodeManager::currentNM()->mkNode( PLUS, children ) : (children.size()==1 ? children[0] : NodeManager::currentNM()->mkConst( Rational(0) ));
+}
+
+// given (msum <k> 0), solve (veq_c * v <k> val) or (val <k> veq_c * v), where:
+// veq_c is either null (meaning 1), or positive.
+// return value -1: veq_c*v is LHS.
+
int QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind k, bool doCoeff ) {
std::map< Node, Node >::iterator itv = msum.find( v );
if( itv!=msum.end() ){
return ires;
}
+/*
+int QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq_c, Node & val, Kind k ) {
+ Assert( k==EQUAL || k==GEQ );
+ std::map< Node, Node >::iterator itv = msum.find( v );
+ if( itv!=msum.end() ){
+ Rational r = itv->second.isNull() ? Rational(1) : itv->second.getConst<Rational>();
+ if( r.sgn()!=0 ){
+ veq_c = itv->second;
+ msum.erase( itv );
+ val = mkNode( msum );
+ msum[v] = veq_c;
+ if( !r.isOne() && !r.isNegativeOne() ){
+ if( v.getType().isInteger() ){
+ veq_c = NodeManager::currentNM()->mkConst( r.abs() );
+ }else{
+ val = NodeManager::currentNM()->mkNode( MULT, val, NodeManager::currentNM()->mkConst( Rational(1) / r.abs() ) );
+ veq_c = Node::null();
+ }
+ }else{
+ veq_c = Node::null();
+ }
+ if( r.sgn()==1 ){
+ val = negate( val );
+ }
+ val = Rewriter::rewrite( val );
+ return ( r.sgn()==1 || k==EQUAL ) ? 1 : -1;
+ }
+ }
+ return 0;
+}
+
+int QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind k, bool doCoeff ) {
+ Node veq_c;
+ Node val;
+ //isolate v in the (in)equality
+ int ires = isolate( v, msum, veq_c, val, k );
+ if( ires!=0 ){
+ Node vc = v;
+ if( !veq_c.isNull() ){
+ if( doCoeff ){
+ vc = NodeManager::currentNM()->mkNode( MULT, veq_c, vc );
+ }else{
+ return 0;
+ }
+ }
+ bool inOrder = ires==1;
+ veq = NodeManager::currentNM()->mkNode( k, inOrder ? vc : val, inOrder ? val : vc );
+ }
+ return ires;
+}
+*/
+
Node QuantArith::solveEqualityFor( Node lit, Node v ) {
Assert( lit.getKind()==EQUAL || lit.getKind()==IFF );
//first look directly at sides
static bool getMonomial( Node n, std::map< Node, Node >& msum );
static bool getMonomialSum( Node n, std::map< Node, Node >& msum );
static bool getMonomialSumLit( Node lit, std::map< Node, Node >& msum );
+ static Node mkNode( std::map< Node, Node >& msum );
//return 1 : solved on LHS, return -1 : solved on RHS, return 0: failed
static int isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind k, bool doCoeff = false );
static int isolate( Node v, std::map< Node, Node >& msum, Node & veq_c, Node & val, Kind k );
Node op = getMatchOperator( n );
d_op_map[op].push_back( n );
added.insert( n );
-
+
if( options::eagerInstQuant() ){
for( unsigned i=0; i<n.getNumChildren(); i++ ){
if( !n.hasAttribute(InstLevelAttribute()) && n.getAttribute(InstLevelAttribute())==0 ){
}
}
-TNode TermDb::evaluateTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep ) {
+//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 ) {
+ std::map< TNode, Node >::iterator itv = visited.find( n );
+ if( itv != visited.end() ){
+ return itv->second;
+ }
+ Node ret;
Trace("term-db-eval") << "evaluate term : " << n << std::endl;
eq::EqualityEngine * ee = d_quantEngine->getTheoryEngine()->getMasterEqualityEngine();
if( ee->hasTerm( n ) ){
Trace("term-db-eval") << "...exists in ee, return rep " << std::endl;
- return ee->getRepresentative( n );
+ ret = ee->getRepresentative( n );
}else if( n.getKind()==BOUND_VARIABLE ){
- Assert( subs.find( n )!=subs.end() );
- Trace("term-db-eval") << "...substitution is : " << subs[n] << std::endl;
- if( subsRep ){
- Assert( ee->hasTerm( subs[n] ) );
- Assert( ee->getRepresentative( subs[n] )==subs[n] );
- return subs[n];
- }else{
- return evaluateTerm( subs[n], subs, subsRep );
+ if( hasSubs ){
+ Assert( subs.find( n )!=subs.end() );
+ Trace("term-db-eval") << "...substitution is : " << subs[n] << std::endl;
+ if( subsRep ){
+ Assert( ee->hasTerm( subs[n] ) );
+ Assert( ee->getRepresentative( subs[n] )==subs[n] );
+ ret = subs[n];
+ }else{
+ ret = evaluateTerm2( subs[n], subs, subsRep, hasSubs, visited );
+ }
}
+ }else if( n.getKind()==FORALL ){
+ ret = n;
}else{
if( n.hasOperator() ){
TNode f = getMatchOperator( n );
- if( !f.isNull() ){
- std::vector< TNode > args;
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- TNode c = evaluateTerm( n[i], subs, subsRep );
- if( c.isNull() ){
- return TNode::null();
- }
- Trace("term-db-eval") << "Got child : " << c << std::endl;
+ 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 );
+ if( c.isNull() ){
+ ret = TNode::null();
+ 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") << "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() ){
- if( ee->hasTerm( nn ) ){
+ }
+ if( !ret_set ){
+ 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() && ee->hasTerm( nn ) ){
Trace("term-db-eval") << "return rep " << std::endl;
- return ee->getRepresentative( nn );
- }else{
- //Assert( false );
+ ret = ee->getRepresentative( nn );
+ ret_set = true;
+ }
+ }
+ if( !ret_set ){
+ //a theory symbol or a new UF term
+ if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+ args.insert( args.begin(), n.getOperator() );
}
+ ret = NodeManager::currentNM()->mkNode( n.getKind(), args );
+ ret = Rewriter::rewrite( ret );
}
}
}
- return TNode::null();
}
+ Trace("term-db-eval") << "evaluated term : " << n << ", got : " << ret << std::endl;
+ visited[n] = ret;
+ return ret;
}
-TNode TermDb::evaluateTerm( TNode n ) {
+
+TNode TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs ) {
+ Trace("term-db-eval") << "evaluate term : " << n << std::endl;
eq::EqualityEngine * ee = d_quantEngine->getTheoryEngine()->getMasterEqualityEngine();
if( ee->hasTerm( n ) ){
- return ee->getRepresentative( n );
- }else if( n.getKind()!=BOUND_VARIABLE ){
+ Trace("term-db-eval") << "...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;
+ if( subsRep ){
+ Assert( ee->hasTerm( subs[n] ) );
+ Assert( ee->getRepresentative( subs[n] )==subs[n] );
+ return subs[n];
+ }else{
+ return evaluateTerm2( subs[n], subs, subsRep, hasSubs );
+ }
+ }
+ }else{
if( n.hasOperator() ){
TNode f = getMatchOperator( n );
if( !f.isNull() ){
std::vector< TNode > args;
for( unsigned i=0; i<n.getNumChildren(); i++ ){
- TNode c = evaluateTerm( n[i] );
+ TNode c = evaluateTerm2( n[i], subs, subsRep, hasSubs );
if( c.isNull() ){
return TNode::null();
}
+ c = ee->getRepresentative( c );
+ Trace("term-db-eval") << "Got child : " << 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;
+ return nn;
if( !nn.isNull() ){
if( ee->hasTerm( nn ) ){
+ Trace("term-db-eval") << "return rep " << std::endl;
return ee->getRepresentative( nn );
}else{
//Assert( false );
return TNode::null();
}
-bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol ) {
+Node TermDb::evaluateTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool mkNewTerms ) {
+ if( mkNewTerms ){
+ std::map< TNode, Node > visited;
+ return evaluateTerm2( n, subs, subsRep, true, visited );
+ }else{
+ return evaluateTerm2( n, subs, subsRep, true );
+ }
+}
+
+Node TermDb::evaluateTerm( TNode n, bool mkNewTerms ) {
+ std::map< TNode, TNode > subs;
+ if( mkNewTerms ){
+ std::map< TNode, Node > visited;
+ return evaluateTerm2( n, subs, false, false, visited );
+ }else{
+ return evaluateTerm2( n, subs, false, false );
+ }
+}
+
+bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol ) {
Trace("term-db-eval") << "Check entailed : " << n << ", pol = " << pol << std::endl;
Assert( n.getType().isBoolean() );
if( n.getKind()==EQUAL ){
- TNode n1 = evaluateTerm( n[0], subs, subsRep );
+ TNode n1 = evaluateTerm2( n[0], subs, subsRep, hasSubs );
if( !n1.isNull() ){
- TNode n2 = evaluateTerm( n[1], subs, subsRep );
+ TNode n2 = evaluateTerm2( n[1], subs, subsRep, hasSubs );
if( !n2.isNull() ){
- eq::EqualityEngine * ee = d_quantEngine->getTheoryEngine()->getMasterEqualityEngine();
- Assert( ee->hasTerm( n1 ) );
- Assert( ee->hasTerm( n2 ) );
- if( pol ){
- return n1==n2 || ee->areEqual( n1, n2 );
+ if( n1==n2 ){
+ return pol;
}else{
- return n1!=n2 && ee->areDisequal( n1, n2, false );
+ eq::EqualityEngine * ee = d_quantEngine->getTheoryEngine()->getMasterEqualityEngine();
+ Assert( ee->hasTerm( n1 ) );
+ Assert( ee->hasTerm( n2 ) );
+ if( pol ){
+ return ee->areEqual( n1, n2 );
+ }else{
+ return ee->areDisequal( n1, n2, false );
+ }
}
}
}
- }else if( n.getKind()==APPLY_UF ){
- TNode n1 = evaluateTerm( n, subs, subsRep );
- if( !n1.isNull() ){
- eq::EqualityEngine * ee = d_quantEngine->getTheoryEngine()->getMasterEqualityEngine();
- Assert( ee->hasTerm( n1 ) );
- TNode n2 = pol ? d_true : d_false;
- if( ee->hasTerm( n2 ) ){
- return ee->areEqual( n1, n2 );
- }
- }
}else if( n.getKind()==NOT ){
- return isEntailed( n[0], subs, subsRep, !pol );
+ return isEntailed( n[0], subs, subsRep, hasSubs, !pol );
}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, pol ) ){
+ if( isEntailed( n[i], subs, subsRep, hasSubs, pol ) ){
if( simPol ){
return true;
}
return !simPol;
}else if( n.getKind()==IFF || n.getKind()==ITE ){
for( unsigned i=0; i<2; i++ ){
- if( isEntailed( n[0], subs, subsRep, i==0 ) ){
+ if( isEntailed( n[0], subs, subsRep, hasSubs, i==0 ) ){
unsigned ch = ( n.getKind()==IFF || i==0 ) ? 1 : 2;
bool reqPol = ( n.getKind()==ITE || i==0 ) ? pol : !pol;
- return isEntailed( n[ch], subs, subsRep, reqPol );
+ return isEntailed( n[ch], subs, subsRep, hasSubs, reqPol );
+ }
+ }
+ }else if( n.getKind()==APPLY_UF ){
+ TNode n1 = evaluateTerm2( n, subs, subsRep, hasSubs );
+ if( !n1.isNull() ){
+ if( n1==d_true ){
+ return pol;
+ }else if( n1==d_false ){
+ return !pol;
+ }else{
+ eq::EqualityEngine * ee = d_quantEngine->getTheoryEngine()->getMasterEqualityEngine();
+ return ee->getRepresentative( n1 ) == ( pol ? d_true : d_false );
}
}
}
return false;
}
+bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol ) {
+ if( d_consistent_ee ){
+ return isEntailed( n, subs, subsRep, true, pol );
+ }else{
+ //don't check entailment wrt an inconsistent ee
+ return false;
+ }
+}
+
bool TermDb::hasTermCurrent( Node n, bool useMode ) {
if( !useMode ){
return d_has_map.find( n )!=d_has_map.end();
}
}
-void TermDb::reset( Theory::Effort effort ){
+bool TermDb::reset( Theory::Effort effort ){
int nonCongruentCount = 0;
int congruentCount = 0;
int alreadyCongruentCount = 0;
d_arg_reps.clear();
d_func_map_trie.clear();
d_func_map_eqc_trie.clear();
+ d_consistent_ee = true;
eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
//compute has map
Trace("term-db-debug") << n << " is redundant." << std::endl;
congruentCount++;
}else{
+ if( at!=n && ee->areDisequal( at, n, false ) ){
+ std::vector< Node > lits;
+ lits.push_back( NodeManager::currentNM()->mkNode( at.getType().isBoolean() ? IFF : EQUAL, at, n ) );
+ for( unsigned i=0; i<at.getNumChildren(); i++ ){
+ if( at[i]!=n[i] ){
+ lits.push_back( NodeManager::currentNM()->mkNode( at[i].getType().isBoolean() ? IFF : EQUAL, at[i], n[i] ).negate() );
+ }
+ }
+ Node lem = lits.size()==1 ? lits[0] : NodeManager::currentNM()->mkNode( OR, lits );
+ if( Trace.isOn("term-db-lemma") ){
+ Trace("term-db-lemma") << "Disequal congruent terms : " << at << " " << n << "!!!!" << std::endl;
+ if( !d_quantEngine->getTheoryEngine()->needCheck() ){
+ Trace("term-db-lemma") << " all theories passed with no lemmas." << std::endl;
+ }
+ Trace("term-db-lemma") << " add lemma : " << lem << std::endl;
+ }
+ d_quantEngine->addLemma( lem );
+ d_consistent_ee = false;
+ return false;
+ }
nonCongruentCount++;
d_op_nonred_count[ it->first ]++;
}
}
}
}
+ return true;
}
TermArgTrie * TermDb::getTermArgTrie( Node f ) {
Trace("quant-attr") << "Attribute : quantifier elimination : " << q << std::endl;
qa.d_quant_elim = true;
//don't set owner, should happen naturally
- }
+ }
if( avar.getAttribute(QuantElimPartialAttribute()) ){
Trace("quant-attr") << "Attribute : quantifier elimination partial : " << q << std::endl;
qa.d_quant_elim = true;
qa.d_quant_elim_partial = true;
//don't set owner, should happen naturally
- }
+ }
if( avar.getKind()==REWRITE_RULE ){
Trace("quant-attr") << "Attribute : rewrite rule : " << q << std::endl;
Assert( i==0 );
std::hash_set< Node, NodeHashFunction > d_iclosure_processed;
/** select op map */
std::map< Node, std::map< TypeNode, Node > > d_par_op_map;
+ /** whether master equality engine is UF-inconsistent */
+ bool d_consistent_ee;
/** set has term */
void setHasTerm( Node n );
+ /** evaluate term */
+ TNode evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs );
+ Node evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, std::map< TNode, Node >& visited );
+ bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol );
public:
TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe );
~TermDb(){}
/** presolve (called once per user check-sat) */
void presolve();
/** reset (calculate which terms are active) */
- void reset( Theory::Effort effort );
+ bool reset( Theory::Effort effort );
/** get match operator */
Node getMatchOperator( Node n );
/** get term arg index */
/** evaluate a term under a substitution. Return representative in EE if possible.
* subsRep is whether subs contains only representatives
*/
- TNode evaluateTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep );
+ Node evaluateTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool mkNewTerms = false );
/** same as above, but without substitution */
- TNode evaluateTerm( TNode n );
+ Node evaluateTerm( TNode n, bool mkNewTerms = false );
/** is entailed (incomplete check) */
bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol );
/** has term */
#include "theory/quantifiers/trigger.h"
#include "theory/quantifiers/quant_split.h"
#include "theory/quantifiers/anti_skolem.h"
+#include "theory/quantifiers/equality_infer.h"
#include "theory/theory_engine.h"
#include "theory/uf/equality_engine.h"
#include "theory/uf/theory_uf.h"
d_presolve_cache(u),
d_presolve_cache_wq(u),
d_presolve_cache_wic(u){
- d_eq_query = new EqualityQueryQuantifiersEngine( this );
+ d_eq_query = new EqualityQueryQuantifiersEngine( c, this );
d_term_db = new quantifiers::TermDb( c, u, this );
d_tr_trie = new inst::TriggerTrie;
d_hasAddedLemma = false;
return;
}
- Trace("quant-engine-debug2") << "Reset term db..." << std::endl;
- d_eq_query->reset( e );
- d_term_db->reset( e );
- if( d_rel_dom ){
- d_rel_dom->reset();
+ if( Trace.isOn("quant-engine-ee-pre") ){
+ Trace("quant-engine-ee-pre") << "Equality engine (pre-inference): " << std::endl;
+ debugPrintEqualityEngine( "quant-engine-ee-pre" );
}
- d_model->reset_round();
+ Trace("quant-engine-debug2") << "Reset equality engine..." << std::endl;
+ d_eq_query->reset( e );
+ if( Trace.isOn("quant-engine-assert") ){
+ Trace("quant-engine-assert") << "Assertions : " << std::endl;
+ getTheoryEngine()->printAssertions("quant-engine-assert");
+ }
if( Trace.isOn("quant-engine-ee") ){
Trace("quant-engine-ee") << "Equality engine : " << std::endl;
debugPrintEqualityEngine( "quant-engine-ee" );
}
- if( Trace.isOn("quant-engine-assert") ){
- Trace("quant-engine-assert") << "Assertions : " << std::endl;
- getTheoryEngine()->printAssertions("quant-engine-assert");
+
+ Trace("quant-engine-debug2") << "Reset term database..." << std::endl;
+ if( !d_term_db->reset( e ) ){
+ flushLemmas();
+ return;
}
+ if( d_rel_dom ){
+ d_rel_dom->reset();
+ }
+ d_model->reset_round();
for( unsigned i=0; i<d_modules.size(); i++ ){
Trace("quant-engine-debug2") << "Reset " << d_modules[i]->identify().c_str() << std::endl;
}
}
+void QuantifiersEngine::notifyCombineTheories() {
+ //if allowing theory combination to happen at most once between instantiation rounds
+ //d_ierCounter = 1;
+ //d_ierCounterLastLc = -1;
+}
+
bool QuantifiersEngine::reduceQuantifier( Node q ) {
std::map< Node, bool >::iterator it = d_quants_red.find( q );
if( it==d_quants_red.end() ){
}
}
+void QuantifiersEngine::eqNotifyNewClass(TNode t) {
+ addTermToDatabase( t );
+ if( d_eq_query->getEqualityInference() ){
+ d_eq_query->getEqualityInference()->eqNotifyNewClass( t );
+ }
+}
+
+void QuantifiersEngine::eqNotifyPreMerge(TNode t1, TNode t2) {
+ if( d_eq_query->getEqualityInference() ){
+ d_eq_query->getEqualityInference()->eqNotifyMerge( t1, t2 );
+ }
+}
+
+void QuantifiersEngine::eqNotifyPostMerge(TNode t1, TNode t2) {
+
+}
+
+void QuantifiersEngine::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
+ //if( d_qcf ){
+ // d_qcf->assertDisequal( t1, t2 );
+ //}
+}
+
void QuantifiersEngine::computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms ){
for( size_t i=0; i<f[0].getNumChildren(); i++ ){
Node n = m.get( i );
Trace("inst-add-debug") << " -> Currently entailed." << std::endl;
return false;
}
+ //Node eval = d_term_db->evaluateTerm( q[1], subs, false, true );
+ //Trace("ajr-temp") << "Instantiation evaluates to : " << std::endl;
+ //Trace("ajr-temp") << " " << eval << std::endl;
}
//check for duplication
}
}
+
+EqualityQueryQuantifiersEngine::EqualityQueryQuantifiersEngine( context::Context* c, QuantifiersEngine* qe ) : d_qe( qe ), d_eqi_counter( c ), d_reset_count( 0 ){
+ if( options::inferArithTriggerEq() ){
+ d_eq_inference = new quantifiers::EqualityInference( c );
+ }else{
+ d_eq_inference = NULL;
+ }
+}
+
+EqualityQueryQuantifiersEngine::~EqualityQueryQuantifiersEngine(){
+ delete d_eq_inference;
+}
+
void EqualityQueryQuantifiersEngine::reset( Theory::Effort e ){
d_int_rep.clear();
d_reset_count++;
void EqualityQueryQuantifiersEngine::processInferences( Theory::Effort e ) {
if( options::inferArithTriggerEq() ){
+ eq::EqualityEngine* ee = getEngine();
+ //naive implementation
+ /*
std::vector< Node > infer;
std::vector< Node > infer_exp;
- eq::EqualityEngine* ee = getEngine();
eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
while( !eqcs_i.isFinished() ){
TNode r = (*eqcs_i);
Trace("quant-engine-ee-proc-debug") << "Asserting equality " << infer[i] << std::endl;
ee->assertEquality( infer[i], true, infer_exp[i] );
}
+ */
+ //updated implementation
+ while( d_eqi_counter.get()<d_eq_inference->d_pending_merges.size() ){
+ Node eq = d_eq_inference->d_pending_merges[d_eqi_counter.get()];
+ Trace("quant-engine-ee-proc") << "processInferences : Infer : " << eq << std::endl;
+ Assert( ee->hasTerm( eq[0] ) );
+ Assert( ee->hasTerm( eq[1] ) );
+ Assert( !ee->areDisequal( eq[0], eq[1], false ) );
+ //just use itself as an explanation for now (should never be used, since equality engine should be consistent)
+ ee->assertEquality( eq, true, eq );
+ d_eqi_counter = d_eqi_counter.get() + 1;
+ }
Assert( ee->consistent() );
}
}
class InstStrategyCegqi;
class QuantDSplit;
class QuantAntiSkolem;
+ class EqualityInference;
}/* CVC4::theory::quantifiers */
namespace inst {
void presolve();
/** check at level */
void check( Theory::Effort e );
+ /** notify that theories were combined */
+ void notifyCombineTheories();
/** register quantifier */
bool registerQuantifier( Node f );
/** register quantifier */
/** get trigger database */
inst::TriggerTrie* getTriggerDatabase() { return d_tr_trie; }
/** add term to database */
- void addTermToDatabase( Node n, bool withinQuant = false, bool withinInstClosure = false );
+ void addTermToDatabase( Node n, bool withinQuant = false, bool withinInstClosure = false );
+ /** notification when master equality engine is updated */
+ void eqNotifyNewClass(TNode t);
+ void eqNotifyPreMerge(TNode t1, TNode t2);
+ void eqNotifyPostMerge(TNode t1, TNode t2);
+ void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
/** get the master equality engine */
eq::EqualityEngine* getMasterEqualityEngine() ;
/** debug print equality engine */
private:
/** pointer to theory engine */
QuantifiersEngine* d_qe;
+ /** quantifiers equality inference */
+ quantifiers::EqualityInference * d_eq_inference;
+ context::CDO< unsigned > d_eqi_counter;
/** internal representatives */
std::map< TypeNode, std::map< Node, Node > > d_int_rep;
/** rep score */
/** get score */
int getRepScore( Node n, Node f, int index, TypeNode v_tn );
public:
- EqualityQueryQuantifiersEngine( QuantifiersEngine* qe ) : d_qe( qe ), d_reset_count( 0 ){}
- ~EqualityQueryQuantifiersEngine(){}
+ EqualityQueryQuantifiersEngine( context::Context* c, QuantifiersEngine* qe );
+ virtual ~EqualityQueryQuantifiersEngine();
/** reset */
void reset( Theory::Effort e );
/** general queries about equality */
Node getInternalRepresentative( Node a, Node f, int index );
/** flatten representatives */
void flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps );
+ /** get quantifiers equality inference */
+ quantifiers::EqualityInference * getEqualityInference() { return d_eq_inference; }
}; /* EqualityQueryQuantifiersEngine */
}/* CVC4::theory namespace */
}
void TheoryEngine::eqNotifyNewClass(TNode t){
- if( d_logicInfo.isQuantified() ){
- d_quantEngine->addTermToDatabase( t );
+ if (d_logicInfo.isQuantified()) {
+ d_quantEngine->eqNotifyNewClass( t );
}
}
void TheoryEngine::eqNotifyPreMerge(TNode t1, TNode t2){
-
+ if (d_logicInfo.isQuantified()) {
+ d_quantEngine->eqNotifyPreMerge( t1, t2 );
+ }
}
void TheoryEngine::eqNotifyPostMerge(TNode t1, TNode t2){
-
+ if (d_logicInfo.isQuantified()) {
+ d_quantEngine->eqNotifyPostMerge( t1, t2 );
+ }
}
void TheoryEngine::eqNotifyDisequal(TNode t1, TNode t2, TNode reason){
- if( d_logicInfo.isQuantified() ){
- if( options::quantConflictFind() ){
- d_quantEngine->getConflictFind()->assertDisequal( t1, t2 );
- }
+ if (d_logicInfo.isQuantified()) {
+ d_quantEngine->eqNotifyDisequal( t1, t2, reason );
}
}
// Do the combination
Debug("theory") << "TheoryEngine::check(" << effort << "): running combination" << endl;
combineTheories();
+ if(d_logicInfo.isQuantified()){
+ d_quantEngine->notifyCombineTheories();
+ }
}
}
// must build model at this point
d_curr_model_builder->buildModel(d_curr_model, true);
}
- Trace("theory::assertions-model") << endl;
+ Trace("theory::assertions-model") << endl;
if (Trace.isOn("theory::assertions-model")) {
printAssertions("theory::assertions-model");
}
projects / cvc5.git / commitdiff