From: ajreynol Date: Mon, 28 Mar 2016 17:32:58 +0000 (-0500) Subject: Implement equality inference module for arithmetic terms. Optimization for entailmen... X-Git-Tag: cvc5-1.0.0~6049^2~85 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=358e453bda62923fd0be94af5317b24a7281014b;p=cvc5.git Implement equality inference module for arithmetic terms. Optimization for entailment checks. Other minor infrastructure. --- diff --git a/src/Makefile.am b/src/Makefile.am index 77c69c9ec..610bcb305 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -362,6 +362,8 @@ libcvc4_la_SOURCES = \ 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 \ diff --git a/src/theory/quantifiers/equality_infer.cpp b/src/theory/quantifiers/equality_infer.cpp new file mode 100644 index 000000000..fc3a274ac --- /dev/null +++ b/src/theory/quantifiers/equality_infer.cpp @@ -0,0 +1,235 @@ +/********************* */ +/*! \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(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; jsize(); 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; isecond->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; + } + } +} + +} diff --git a/src/theory/quantifiers/equality_infer.h b/src/theory/quantifiers/equality_infer.h new file mode 100644 index 000000000..4a6943119 --- /dev/null +++ b/src/theory/quantifiers/equality_infer.h @@ -0,0 +1,77 @@ +/********************* */ +/*! \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 +#include +#include +#include + +#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 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 diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index bf91f74c6..3d649f302 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -33,11 +33,16 @@ bool QuantArith::getMonomial( Node n, Node& c, Node& v ){ } } 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(); @@ -63,10 +68,7 @@ bool QuantArith::getMonomialSum( Node n, std::map< Node, Node >& msum ) { 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().isZero() ){ - msum[Node::null()] = negate( lit[1] ); - } + if( lit[1].isConst() && lit[1].getConst().isZero() ){ return true; }else{ //subtract the other side @@ -90,6 +92,29 @@ bool QuantArith::getMonomialSumLit( Node lit, std::map< Node, Node >& msum ) { 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 0), solve (veq_c * v val) or (val 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() ){ @@ -155,6 +180,58 @@ int QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq_c, Nod 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(); + 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 diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index b4cf54dfd..0327651d7 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -36,6 +36,7 @@ public: 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 ); diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 0d7c9352c..a2ce9c368 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -151,7 +151,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool wi Node op = getMatchOperator( n ); d_op_map[op].push_back( n ); added.insert( n ); - + if( options::eagerInstQuant() ){ for( unsigned i=0; i& 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 args; + bool ret_set = false; + for( unsigned i=0; ihasTerm( 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; igetRepresentative( 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 ); @@ -281,40 +333,53 @@ TNode TermDb::evaluateTerm( TNode n ) { 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& 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, 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(); @@ -435,7 +521,7 @@ void TermDb::presolve() { } } -void TermDb::reset( Theory::Effort effort ){ +bool TermDb::reset( Theory::Effort effort ){ int nonCongruentCount = 0; int congruentCount = 0; int alreadyCongruentCount = 0; @@ -444,6 +530,7 @@ void TermDb::reset( Theory::Effort effort ){ 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 @@ -517,6 +604,26 @@ void TermDb::reset( Theory::Effort effort ){ 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; imkNode( 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 ]++; } @@ -543,6 +650,7 @@ void TermDb::reset( Theory::Effort effort ){ } } } + return true; } TermArgTrie * TermDb::getTermArgTrie( Node f ) { @@ -1914,13 +2022,13 @@ void TermDb::computeQuantAttributes( Node q, QAttributes& qa ){ 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 ); diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 6b8f9c783..62da8c347 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -174,8 +174,14 @@ private: 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(){} @@ -213,7 +219,7 @@ public: /** 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 */ @@ -228,9 +234,9 @@ public: /** 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 */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 1aeb6f517..86e15485a 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -41,6 +41,7 @@ #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" @@ -97,7 +98,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* 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; @@ -411,22 +412,31 @@ void QuantifiersEngine::check( Theory::Effort e ){ 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; iidentify().c_str() << std::endl; @@ -549,6 +559,12 @@ void QuantifiersEngine::check( Theory::Effort e ){ } } +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() ){ @@ -703,6 +719,29 @@ void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool within } } +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& terms, bo 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 @@ -1253,6 +1295,19 @@ void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) { } } + +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++; @@ -1261,9 +1316,11 @@ void EqualityQueryQuantifiersEngine::reset( Theory::Effort e ){ 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); @@ -1309,6 +1366,18 @@ void EqualityQueryQuantifiersEngine::processInferences( Theory::Effort e ) { 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_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() ); } } diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 920c45c1a..afde8c996 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -102,6 +102,7 @@ namespace quantifiers { class InstStrategyCegqi; class QuantDSplit; class QuantAntiSkolem; + class EqualityInference; }/* CVC4::theory::quantifiers */ namespace inst { @@ -284,6 +285,8 @@ public: 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 */ @@ -348,7 +351,12 @@ public: /** 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 */ @@ -394,6 +402,9 @@ class EqualityQueryQuantifiersEngine : public EqualityQuery 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 */ @@ -408,8 +419,8 @@ private: /** 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 */ @@ -426,6 +437,8 @@ public: 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 */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 045af0864..c539315af 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -78,24 +78,26 @@ void TheoryEngine::finishInit() { } 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 ); } } @@ -405,6 +407,9 @@ void TheoryEngine::check(Theory::Effort effort) { // Do the combination Debug("theory") << "TheoryEngine::check(" << effort << "): running combination" << endl; combineTheories(); + if(d_logicInfo.isQuantified()){ + d_quantEngine->notifyCombineTheories(); + } } } @@ -419,7 +424,7 @@ void TheoryEngine::check(Theory::Effort effort) { // 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"); }