summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r--src/theory/quantifiers/equality_infer.h13
-rw-r--r--src/theory/quantifiers/quant_util.cpp71
-rw-r--r--src/theory/quantifiers/quant_util.h2
-rw-r--r--src/theory/quantifiers/term_database.cpp8
4 files changed, 16 insertions, 78 deletions
diff --git a/src/theory/quantifiers/equality_infer.h b/src/theory/quantifiers/equality_infer.h
index 4a6943119..70b05c351 100644
--- a/src/theory/quantifiers/equality_infer.h
+++ b/src/theory/quantifiers/equality_infer.h
@@ -14,8 +14,8 @@
#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>
@@ -60,14 +60,17 @@ private:
/** 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]; }
};
}
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index 3d649f302..1f1efa2a8 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -113,9 +113,8 @@ Node QuantArith::mkNode( std::map< Node, Node >& msum ) {
// 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;
@@ -136,75 +135,20 @@ int QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind
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;
}
}
@@ -230,7 +174,6 @@ int QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind
}
return ires;
}
-*/
Node QuantArith::solveEqualityFor( Node lit, Node v ) {
Assert( lit.getKind()==EQUAL || lit.getKind()==IFF );
@@ -241,7 +184,7 @@ Node QuantArith::solveEqualityFor( Node lit, Node v ) {
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 ) ){
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index 0327651d7..31743d352 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -38,8 +38,8 @@ public:
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 );
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index a2ce9c368..3b74cf352 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -319,14 +319,6 @@ TNode TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsR
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 );
- }
- }
}
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback