Trace("smt") << "turning on quantifier logic, for strings-exp"
<< std::endl;
}
- if(! options::finiteModelFind.wasSetByUser()) {
- options::finiteModelFind.set( true );
- Trace("smt") << "turning on finite-model-find, for strings-exp"
- << std::endl;
- }
if(! options::fmfBoundInt.wasSetByUser()) {
- if(! options::fmfBoundIntLazy.wasSetByUser()) {
- options::fmfBoundIntLazy.set( true );
- }
options::fmfBoundInt.set( true );
Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl;
}
d_dt.conflict(t1, t2);
}
void eqNotifyNewClass(TNode t) {
- Debug("dt") << "NotifyClass::eqNotifyNewClass(" << t << std::endl;
+ Debug("dt") << "NotifyClass::eqNotifyNewClass(" << t << ")" << std::endl;
d_dt.eqNotifyNewClass(t);
}
void eqNotifyPreMerge(TNode t1, TNode t2) {
- Debug("dt") << "NotifyClass::eqNotifyPreMerge(" << t1 << ", " << t2 << std::endl;
+ Debug("dt") << "NotifyClass::eqNotifyPreMerge(" << t1 << ", " << t2 << ")" << std::endl;
d_dt.eqNotifyPreMerge(t1, t2);
}
void eqNotifyPostMerge(TNode t1, TNode t2) {
- Debug("dt") << "NotifyClass::eqNotifyPostMerge(" << t1 << ", " << t2 << std::endl;
+ Debug("dt") << "NotifyClass::eqNotifyPostMerge(" << t1 << ", " << t2 << ")" << std::endl;
d_dt.eqNotifyPostMerge(t1, t2);
}
void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
- Debug("dt") << "NotifyClass::eqNotifyDisequal(" << t1 << ", " << t2 << ", " << reason << std::endl;
+ Debug("dt") << "NotifyClass::eqNotifyDisequal(" << t1 << ", " << t2 << ", " << reason << ")" << std::endl;
d_dt.eqNotifyDisequal(t1, t2, reason);
}
};/* class TheoryDatatypes::NotifyClass */
#include "cvc4_private.h"
-#ifndef EQUALITY_INFER_H
-#define EQUALITY_INFER_H
+#ifndef __CVC4__THEORY__QUANTIFIERS__EQUALITY_INFER_H
+#define __CVC4__THEORY__QUANTIFIERS__EQUALITY_INFER_H
#include <ext/hash_set>
#include <iostream>
/** use list */
NodeListMap d_uselist;
void addToUseList( Node used, Node eqc );
+ /** pending merges */
+ NodeList d_pending_merges;
public:
EqualityInference(context::Context* c);
virtual ~EqualityInference();
- /** notification when equality engine is updated */
+ /** input : notification when equality engine is updated */
void eqNotifyNewClass(TNode t);
void eqNotifyMerge(TNode t1, TNode t2);
-
- NodeList d_pending_merges;
+ /** output : inferred equalities */
+ unsigned getNumPendingMerges() { return d_pending_merges.size(); }
+ Node getPendingMerge( unsigned i ) { return d_pending_merges[i]; }
};
}
// 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 ) {
+// return value 1: veq_c*v is RHS, -1: veq_c*v is LHS, 0: failed.
+int QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq_c, Node & val, Kind k ) {
std::map< Node, Node >::iterator itv = msum.find( v );
if( itv!=msum.end() ){
std::vector< Node > children;
children.push_back(m);
}
}
- veq = children.size()>1 ? NodeManager::currentNM()->mkNode( PLUS, children ) :
+ val = children.size()>1 ? NodeManager::currentNM()->mkNode( PLUS, children ) :
(children.size()==1 ? children[0] : NodeManager::currentNM()->mkConst( Rational(0) ));
- Node vc = v;
- if( !r.isOne() && !r.isNegativeOne() ){
- if( vc.getType().isInteger() ){
- if( doCoeff ){
- vc = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( r.abs() ), vc );
- }else{
- return 0;
- }
- }else{
- veq = NodeManager::currentNM()->mkNode( MULT, veq, NodeManager::currentNM()->mkConst( Rational(1) / r.abs() ) );
- }
- }
- if( r.sgn()==1 ){
- veq = negate(veq);
- }
- veq = Rewriter::rewrite( veq );
- bool inOrder = r.sgn()==1 || k==EQUAL;
- veq = NodeManager::currentNM()->mkNode( k, inOrder ? vc : veq, inOrder ? veq : vc );
- return inOrder ? 1 : -1;
- }
- }
- return 0;
-}
-
-int QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq_c, Node & val, Kind k ) {
- Node vatom;
- //isolate pv in the inequality
- int ires = isolate( v, msum, vatom, k, true );
- if( ires!=0 ){
- val = vatom[ ires==1 ? 1 : 0 ];
- Node pvm = vatom[ ires==1 ? 0 : 1 ];
- //get monomial
- if( pvm!=v ){
- Node veq_v;
- if( QuantArith::getMonomial( pvm, veq_c, veq_v ) ){
- Assert( veq_v==v );
- }
- }
- }
- 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 = negate(val);
+ }else{
+ val = Rewriter::rewrite( val );
}
- val = Rewriter::rewrite( val );
return ( r.sgn()==1 || k==EQUAL ) ? 1 : -1;
}
}
}
return ires;
}
-*/
Node QuantArith::solveEqualityFor( Node lit, Node v ) {
Assert( lit.getKind()==EQUAL || lit.getKind()==IFF );
return lit[1-r];
}
}
- if( tn.isInteger() || tn.isReal() ){
+ if( tn.isReal() ){
if( quantifiers::TermDb::containsTerm( lit, v ) ){
std::map< Node, Node > msum;
if( QuantArith::getMonomialSumLit( lit, 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 );
+ static int isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind k, bool doCoeff = false );
static Node solveEqualityFor( Node lit, Node v );
static Node negate( Node t );
static Node offset( Node t, int i );
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 );
- }
- }
}
}
}
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::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
- while( !eqcs_i.isFinished() ){
- TNode r = (*eqcs_i);
- TypeNode tr = r.getType();
- if( tr.isReal() ){
- std::vector< Node > eqc;
- eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
- while( !eqc_i.isFinished() ){
- TNode n = (*eqc_i);
- //accumulate equivalence class
- eqc.push_back( n );
- ++eqc_i;
- }
- for( unsigned i=0; i<eqc.size(); i++ ){
- Node n = eqc[i];
- if( n.getKind()==PLUS ){
- std::map< Node, Node > msum;
- QuantArith::getMonomialSum( n, msum );
- for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
- //if the term is a trigger
- Node t = it->first;
- if( inst::Trigger::isAtomicTrigger( t ) ){
- for( unsigned j=0; j<eqc.size(); j++ ){
- if( i!=j ){
- Node eq = n.eqNode( eqc[j] );
- Node v = QuantArith::solveEqualityFor( eq, t );
- Trace("quant-engine-ee-proc-debug") << "processInferences : Can infer : " << t << " == " << v << std::endl;
- if( ee->hasTerm( v ) && ee->getRepresentative( v )!=r ){
- Trace("quant-engine-ee-proc") << "processInferences : Infer : " << t << " == " << v << " from " << n << " == " << eqc[j] << std::endl;
- infer.push_back( t.eqNode( v ) );
- infer_exp.push_back( n.eqNode( eqc[j] ) );
- }
- }
- }
- }
- }
- }
- }
- }
- ++eqcs_i;
- }
- for( unsigned i=0; i<infer.size(); 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()];
+ while( d_eqi_counter.get()<d_eq_inference->getNumPendingMerges() ){
+ Node eq = d_eq_inference->getPendingMerge( d_eqi_counter.get() );
Trace("quant-engine-ee-proc") << "processInferences : Infer : " << eq << std::endl;
Assert( ee->hasTerm( eq[0] ) );
Assert( ee->hasTerm( eq[1] ) );
Node a = d_nodes[currentNode];
Node b = d_nodes[d_equalityEdges[currentEdge].getNodeId()];
- if (d_pathReconstructionTriggers.find(reasonType) != d_pathReconstructionTriggers.end()) {
- d_pathReconstructionTriggers.find(reasonType)->second->notify(reasonType, reason, a, b,
- equalities, eqpc);
- }
-
if (eqpc) {
+ //apply proof reconstruction processing (when eqpc is non-null)
+ if (d_pathReconstructionTriggers.find(reasonType) != d_pathReconstructionTriggers.end()) {
+ d_pathReconstructionTriggers.find(reasonType)->second->notify(reasonType, reason, a, b,
+ equalities, eqpc);
+ }
if (reasonType == MERGED_THROUGH_EQUALITY) {
eqpc->d_node = reason;
} else {
projects / cvc5.git / commitdiff