summaryrefslogtreecommitdiff
path: root/src/theory/uf
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/uf')
-rw-r--r--src/theory/uf/equality_engine.h38
-rw-r--r--src/theory/uf/kinds45
-rw-r--r--src/theory/uf/options18
-rw-r--r--src/theory/uf/theory_uf.cpp73
-rw-r--r--src/theory/uf/theory_uf.h4
-rw-r--r--src/theory/uf/theory_uf_model.cpp75
-rw-r--r--src/theory/uf/theory_uf_model.h18
-rw-r--r--src/theory/uf/theory_uf_strong_solver.cpp1556
-rw-r--r--src/theory/uf/theory_uf_strong_solver.h230
-rw-r--r--src/theory/uf/theory_uf_type_rules.h62
10 files changed, 1263 insertions, 856 deletions
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 1e3b276a4..45d1b4acf 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -82,7 +82,7 @@ public:
virtual bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) = 0;
/**
- * Notifies about the merge of two constant terms. After this, all work is suspended and all you
+ * Notifies about the merge of two constant terms. After this, all work is suspended and all you
* can do is ask for explanations.
*
* @param t1 a constant term
@@ -384,7 +384,7 @@ private:
std::vector<TriggerId> d_nodeTriggers;
/**
- * Map from ids to whether they are constants (constants are always
+ * Map from ids to whether they are constants (constants are always
* representatives of their class.
*/
std::vector<bool> d_isConstant;
@@ -427,7 +427,7 @@ private:
/**
* Get an explanation of the equality t1 = t2. Returns the asserted equalities that
* imply t1 = t2. Returns TNodes as the assertion equalities should be hashed somewhere
- * else.
+ * else.
*/
void getExplanation(EqualityEdgeId t1Id, EqualityNodeId t2Id, std::vector<TNode>& equalities) const;
@@ -440,7 +440,7 @@ private:
Node d_true;
/** True node id */
EqualityNodeId d_trueId;
-
+
/** The false node */
Node d_false;
/** False node id */
@@ -484,12 +484,12 @@ private:
/** Internal tags for creating a new set */
Theory::Set d_newSetTags;
-
+
/** Internal triggers for creating a new set */
EqualityNodeId d_newSetTriggers[THEORY_LAST];
-
+
/** Size of the internal triggers array */
- unsigned d_newSetTriggersSize;
+ unsigned d_newSetTriggersSize;
/** The information about trigger terms is stored in this easily maintained memory. */
char* d_triggerDatabase;
@@ -524,7 +524,7 @@ private:
struct TriggerSetUpdate {
EqualityNodeId classId;
TriggerTermSetRef oldValue;
- TriggerSetUpdate(EqualityNodeId classId = null_id, TriggerTermSetRef oldValue = null_set_id)
+ TriggerSetUpdate(EqualityNodeId classId = null_id, TriggerTermSetRef oldValue = null_set_id)
: classId(classId), oldValue(oldValue) {}
};/* struct EqualityEngine::TriggerSetUpdate */
@@ -591,7 +591,7 @@ private:
* reasons should be pushed on the reasons vector.
*/
void storePropagatedDisequality(TheoryId tag, EqualityNodeId lhsId, EqualityNodeId rhsId);
-
+
/**
* An equality tagged with a set of tags.
*/
@@ -599,10 +599,10 @@ private:
/** Id of the equality */
EqualityNodeId equalityId;
/** TriggerSet reference for the class of one of the sides */
- TriggerTermSetRef triggerSetRef;
+ TriggerTermSetRef triggerSetRef;
/** Is trigger equivalent to the lhs (rhs otherwise) */
bool lhs;
-
+
TaggedEquality(EqualityNodeId equalityId = null_id, TriggerTermSetRef triggerSetRef = null_set_id, bool lhs = true)
: equalityId(equalityId), triggerSetRef(triggerSetRef), lhs(lhs) {}
};
@@ -625,9 +625,9 @@ private:
/**
* Propagates the remembered disequalities with given tags the original triggers for those tags,
- * and the set of disequalities produced by above.
+ * and the set of disequalities produced by above.
*/
- bool propagateTriggerTermDisequalities(Theory::Set tags,
+ bool propagateTriggerTermDisequalities(Theory::Set tags,
TriggerTermSetRef triggerSetRef, const TaggedEqualitiesSet& disequalitiesToNotify);
/** Name of the equality engine */
@@ -636,12 +636,12 @@ private:
public:
/**
- * Initialize the equality engine, given the notification class.
+ * Initialize the equality engine, given the notification class.
*/
EqualityEngine(EqualityEngineNotify& notify, context::Context* context, std::string name);
/**
- * Initialize the equality engine with no notification class.
+ * Initialize the equality engine with no notification class.
*/
EqualityEngine(context::Context* context, std::string name);
@@ -791,7 +791,7 @@ class EqClassesIterator {
const eq::EqualityEngine* d_ee;
size_t d_it;
-
+ std::vector< Node > d_visited;
public:
EqClassesIterator(): d_ee(NULL), d_it(0){ }
@@ -812,11 +812,11 @@ public:
return !(*this == i);
}
EqClassesIterator& operator++() {
- Node orig = d_ee->d_nodes[d_it];
+ d_visited.push_back( d_ee->d_nodes[d_it] );
++d_it;
while ( d_it<d_ee->d_nodesCount &&
- ( d_ee->getRepresentative(d_ee->d_nodes[d_it]) != d_ee->d_nodes[d_it]
- || d_ee->d_nodes[d_it] == orig ) ) { // this line is necessary for ignoring duplicates
+ ( d_ee->getRepresentative(d_ee->d_nodes[d_it]) != d_ee->d_nodes[d_it] ||
+ std::find( d_visited.begin(), d_visited.end(), d_ee->d_nodes[d_it] )!=d_visited.end() ) ) { // this line is necessary for ignoring duplicates
++d_it;
}
return *this;
diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds
index efad8beb9..1d179248c 100644
--- a/src/theory/uf/kinds
+++ b/src/theory/uf/kinds
@@ -9,7 +9,7 @@ typechecker "theory/uf/theory_uf_type_rules.h"
instantiator ::CVC4::theory::uf::InstantiatorTheoryUf "theory/uf/theory_uf_instantiator.h"
properties stable-infinite parametric
-properties check propagate ppStaticLearn presolve
+properties check propagate ppStaticLearn presolve getNextDecisionRequest
rewriter ::CVC4::theory::uf::TheoryUfRewriter "theory/uf/theory_uf_rewriter.h"
parameterized APPLY_UF VARIABLE 1: "uninterpreted function application"
@@ -19,47 +19,4 @@ typerule APPLY_UF ::CVC4::theory::uf::UfTypeRule
operator CARDINALITY_CONSTRAINT 2 "cardinality constraint"
typerule CARDINALITY_CONSTRAINT ::CVC4::theory::uf::CardinalityConstraintTypeRule
-#
-# For compact function models
-# There are three cases for FUNCTION_MODEL nodes:
-# (1) The node has two children, the first being of kind FUNCTION_CASE_SPLIT. The second child specifies a default value.
-# (2) The node has one child of kind FUNCTION_CASE_SPLIT.
-# (3) The node has one child, it's default value.
-#
-# Semantics of FUNCTION_MODEL kind-ed nodes. The value of n applied to arguments args is
-#
-# getValueFM( n, args, 0 ), where:
-#
-# Node getValueFM( n, args, argIndex )
-# if n.getKind()!=FUNCTION_MODEL
-# return n;
-# else if (1)
-# val = getValueFCS( n[0], args, argIndex );
-# if !val.isNull()
-# return val;
-# else
-# return getValueFM( n[1], args, argIndex+1 );
-# else if (2)
-# return getValueFCS( n[0], args, argIndex );
-# else if (3)
-# return getValueFM( n[0], args, argIndex+1 );
-#
-# Node getValueFCS( n, args, argIndex ) :
-# //n.getKind()==FUNCTION_CASE_SPLIT
-# //n[j].getKind()==FUNCTION_CASE for all 0<=j<n.getNumChildren()
-# if( args[argIndex]=n[i][0] for some i)
-# return getValueFM( n[i][1], args, argIndex+1 );
-# else
-# return null;
-#
-
-operator FUNCTION_MODEL 1:2 "function model"
-typerule FUNCTION_MODEL ::CVC4::theory::uf::FunctionModelTypeRule
-
-operator FUNCTION_CASE_SPLIT 1: "function case split"
-typerule FUNCTION_CASE_SPLIT ::CVC4::theory::uf::FunctionCaseSplitTypeRule
-
-operator FUNCTION_CASE 2 "function case"
-typerule FUNCTION_CASE ::CVC4::theory::uf::FunctionCaseTypeRule
-
endtheory
diff --git a/src/theory/uf/options b/src/theory/uf/options
index 6f6900da0..8185f0b3d 100644
--- a/src/theory/uf/options
+++ b/src/theory/uf/options
@@ -9,4 +9,22 @@ option ufSymmetryBreaker uf-symmetry-breaker --enable-symmetry-breaker/--disable
use UF symmetry breaker (Deharbe et al., CADE 2011)
/turns off UF symmetry breaker (Deharbe et al., CADE 2011)
+option ufssRegions /--disable-uf-ss-regions bool :default true
+ disable region-based method for discovering cliques and splits in uf strong solver
+option ufssEagerSplits --uf-ss-eager-split bool :default false
+ add splits eagerly for uf strong solver
+option ufssColoringSat --uf-ss-coloring-sat bool :default false
+ use coloring-based SAT heuristic for uf strong solver
+option ufssTotality --uf-ss-totality bool :default false
+ use totality axioms for enforcing cardinality constraints
+option ufssTotalityLazy --uf-ss-totality-lazy bool :default false
+ apply totality axioms lazily
+option ufssAbortCardinality --uf-ss-abort-card=N int :default -1
+ tells the uf strong solver a cardinality to abort at (-1 == no limit, default)
+option ufssSmartSplits --uf-ss-smart-split bool :default false
+ use smart splitting heuristic for uf strong solver
+option ufssModelInference --uf-ss-model-infer bool :default false
+ use model inference method for uf strong solver
+
+
endmodule
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 5b8470567..a1500e084 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -23,6 +23,7 @@
#include "theory/uf/theory_uf_instantiator.h"
#include "theory/uf/theory_uf_strong_solver.h"
#include "theory/model.h"
+#include "theory/type_enumerator.h"
using namespace std;
using namespace CVC4;
@@ -80,6 +81,10 @@ void TheoryUF::check(Effort level) {
if (d_thss != NULL) {
bool isDecision = d_valuation.isSatLiteral(fact) && d_valuation.isDecision(fact);
d_thss->assertNode(fact, isDecision);
+ if( d_thss->isConflict() ){
+ d_conflict = true;
+ return;
+ }
}
// Do the work
@@ -98,6 +103,9 @@ void TheoryUF::check(Effort level) {
if (d_thss != NULL) {
if (! d_conflict) {
d_thss->check(level);
+ if( d_thss->isConflict() ){
+ d_conflict = true;
+ }
}
}
@@ -127,6 +135,9 @@ void TheoryUF::preRegisterTerm(TNode node) {
// Remember the function and predicate terms
d_functionsTerms.push_back(node);
break;
+ case kind::CARDINALITY_CONSTRAINT:
+ //do nothing
+ break;
default:
// Variables etc
d_equalityEngine.addTerm(node);
@@ -150,8 +161,16 @@ bool TheoryUF::propagate(TNode literal) {
}/* TheoryUF::propagate(TNode) */
void TheoryUF::propagate(Effort effort) {
- if (d_thss != NULL) {
- return d_thss->propagate(effort);
+ //if (d_thss != NULL) {
+ // return d_thss->propagate(effort);
+ //}
+}
+
+Node TheoryUF::getNextDecisionRequest(){
+ if (d_thss != NULL && !d_conflict) {
+ return d_thss->getNextDecisionRequest();
+ }else{
+ return Node::null();
}
}
@@ -173,8 +192,55 @@ Node TheoryUF::explain(TNode literal) {
return mkAnd(assumptions);
}
-void TheoryUF::collectModelInfo( TheoryModel* m ){
+void TheoryUF::collectModelInfo( TheoryModel* m, bool fullModel ){
m->assertEqualityEngine( &d_equalityEngine );
+ if( fullModel ){
+#if 1
+ std::map< TypeNode, int > type_count;
+ //must choose proper representatives
+ // for each equivalence class, specify the constructor as a representative
+ eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
+ while( !eqcs_i.isFinished() ){
+ Node eqc = (*eqcs_i);
+ TypeNode tn = eqc.getType();
+ if( tn.isSort() ){
+ if( type_count.find( tn )==type_count.end() ){
+ type_count[tn] = 0;
+ }
+ std::stringstream ss;
+ ss << Expr::setlanguage(options::outputLanguage());
+ ss << "$t_" << tn << (type_count[tn]+1);
+ type_count[tn]++;
+ Node rep = NodeManager::currentNM()->mkSkolem( ss.str(), tn );
+ Trace("mkVar") << "TheoryUF::collectModelInfo: make variable " << rep << " : " << tn << std::endl;
+ //specify the constant as the representative
+ m->assertEquality( eqc, rep, true );
+ m->assertRepresentative( rep );
+ }
+ ++eqcs_i;
+ }
+#else
+ std::map< TypeNode, TypeEnumerator* > type_enums;
+ //must choose proper representatives
+ // for each equivalence class, specify the constructor as a representative
+ eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
+ while( !eqcs_i.isFinished() ){
+ Node eqc = (*eqcs_i);
+ TypeNode tn = eqc.getType();
+ if( tn.isSort() ){
+ if( type_enums.find( tn )==type_enums.end() ){
+ type_enums[tn] = new TypeEnumerator( tn );
+ }
+ Node rep = *(*type_enums[tn]);
+ ++(*type_enums[tn]);
+ //specify the constant as the representative
+ m->assertEquality( eqc, rep, true );
+ m->assertRepresentative( rep );
+ }
+ ++eqcs_i;
+ }
+ #endif
+ }
}
void TheoryUF::presolve() {
@@ -481,3 +547,4 @@ Node TheoryUF::ppRewrite(TNode node) {
}
}
}
+
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 604b1f44c..62ca640aa 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -193,7 +193,7 @@ public:
void preRegisterTerm(TNode term);
Node explain(TNode n);
- void collectModelInfo( TheoryModel* m );
+ void collectModelInfo( TheoryModel* m, bool fullModel );
void ppStaticLearn(TNode in, NodeBuilder<>& learned);
void presolve();
@@ -202,6 +202,7 @@ public:
void computeCareGraph();
void propagate(Effort effort);
+ Node getNextDecisionRequest();
EqualityStatus getEqualityStatus(TNode a, TNode b);
@@ -226,7 +227,6 @@ public:
void registerPpRewrite(TNode op, PpRewrite* callback) {
d_registeredPpRewrites.insert(std::make_pair(op, callback));
}
-
};/* class TheoryUF */
}/* CVC4::theory::uf namespace */
diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp
index 0082f4840..b8110a2aa 100644
--- a/src/theory/uf/theory_uf_model.cpp
+++ b/src/theory/uf/theory_uf_model.cpp
@@ -136,35 +136,46 @@ Node UfModelTreeNode::getValue( TheoryModel* m, Node n, std::vector< int >& inde
}
}
-Node UfModelTreeNode::getFunctionValue(){
+Node UfModelTreeNode::getFunctionValue( std::vector< Node >& args, int index, Node argDefaultValue ){
if( !d_data.empty() ){
- Node defaultValue;
+ Node defaultValue = argDefaultValue;
+ if( d_data.find( Node::null() )!=d_data.end() ){
+ defaultValue = d_data[Node::null()].getFunctionValue( args, index+1, argDefaultValue );
+ }
std::vector< Node > caseValues;
+ std::map< Node, Node > caseArg;
for( std::map< Node, UfModelTreeNode >::iterator it = d_data.begin(); it != d_data.end(); ++it ){
- if( it->first.isNull() ){
- defaultValue = it->second.getFunctionValue();
- }else{
- caseValues.push_back( NodeManager::currentNM()->mkNode( FUNCTION_CASE, it->first, it->second.getFunctionValue() ) );
+ if( !it->first.isNull() ){
+ Node val = it->second.getFunctionValue( args, index+1, defaultValue );
+ caseValues.push_back( val );
+ caseArg[ val ] = it->first;
}
}
- if( caseValues.empty() && defaultValue.getKind()!=FUNCTION_CASE_SPLIT && defaultValue.getKind()!=FUNCTION_MODEL ){
- return defaultValue;
- }else{
- std::vector< Node > children;
- if( !caseValues.empty() ){
- children.push_back( NodeManager::currentNM()->mkNode( FUNCTION_CASE_SPLIT, caseValues ) );
- }
- if( !defaultValue.isNull() ){
- children.push_back( defaultValue );
- }
- return NodeManager::currentNM()->mkNode( FUNCTION_MODEL, children );
+ Node retNode = defaultValue;
+ for( int i=((int)caseValues.size()-1); i>=0; i-- ){
+ retNode = NodeManager::currentNM()->mkNode( ITE, args[index].eqNode( caseArg[ caseValues[i] ] ), caseValues[i], retNode );
}
+ return retNode;
}else{
Assert( !d_value.isNull() );
return d_value;
}
}
+//update function
+void UfModelTreeNode::update( TheoryModel* m ){
+ if( !d_value.isNull() ){
+ d_value = m->getRepresentative( d_value );
+ }
+ std::map< Node, UfModelTreeNode > old = d_data;
+ d_data.clear();
+ for( std::map< Node, UfModelTreeNode >::iterator it = old.begin(); it != old.end(); ++it ){
+ Node rep = m->getRepresentative( it->first );
+ d_data[ rep ] = it->second;
+ d_data[ rep ].update( m );
+ }
+}
+
//simplify function
void UfModelTreeNode::simplify( Node op, Node defaultVal, int argIndex ){
if( argIndex<(int)op.getType().getNumChildren()-1 ){
@@ -251,31 +262,17 @@ void UfModelTreeNode::debugPrint( std::ostream& out, TheoryModel* m, std::vector
}
}
-
-Node UfModelTree::toIte2( Node fm_node, std::vector< Node >& args, int index, Node defaultNode ){
- if( fm_node.getKind()==FUNCTION_MODEL ){
- if( fm_node[0].getKind()==FUNCTION_CASE_SPLIT ){
- Node retNode;
- Node childDefaultNode = defaultNode;
- //get new default
- if( fm_node.getNumChildren()==2 ){
- childDefaultNode = toIte2( fm_node[1], args, index+1, defaultNode );
- }
- retNode = childDefaultNode;
- for( int i=(int)fm_node[0].getNumChildren()-1; i>=0; i-- ){
- Node childNode = toIte2( fm_node[0][1], args, index+1, childDefaultNode );
- retNode = NodeManager::currentNM()->mkNode( ITE, args[index].eqNode( fm_node[0][0] ), childNode, retNode );
- }
- return retNode;
- }else{
- return toIte2( fm_node[0], args, index+1, defaultNode );
- }
- }else{
- return fm_node;
+Node UfModelTree::getFunctionValue( const char* argPrefix ){
+ TypeNode type = d_op.getType();
+ std::vector< Node > vars;
+ for( size_t i=0; i<type.getNumChildren()-1; i++ ){
+ std::stringstream ss;
+ ss << argPrefix << (i+1);
+ vars.push_back( NodeManager::currentNM()->mkSkolem( ss.str(), type[i] ) );
}
+ return getFunctionValue( vars );
}
-
Node UfModelTreeGenerator::getIntersection( TheoryModel* m, Node n1, Node n2, bool& isGround ){
//Notice() << "Get intersection " << n1 << " " << n2 << std::endl;
isGround = true;
diff --git a/src/theory/uf/theory_uf_model.h b/src/theory/uf/theory_uf_model.h
index 9dba16608..61c0714a3 100644
--- a/src/theory/uf/theory_uf_model.h
+++ b/src/theory/uf/theory_uf_model.h
@@ -48,7 +48,9 @@ public:
/** getConstant Value function */
Node getConstantValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int argIndex );
/** getFunctionValue */
- Node getFunctionValue();
+ Node getFunctionValue( std::vector< Node >& args, int index, Node argDefaultValue );
+ /** update function */
+ void update( TheoryModel* m );
/** simplify function */
void simplify( Node op, Node defaultVal, int argIndex );
/** is total ? */
@@ -123,12 +125,15 @@ public:
return d_tree.getConstantValue( m, n, d_index_order, 0 );
}
/** getFunctionValue
- * Returns a compact representation of this function, of kind FUNCTION_MODEL.
- * See documentation in theory/uf/kinds
+ * Returns a representation of this function.
*/
- Node getFunctionValue(){
- return d_tree.getFunctionValue();
- }
+ Node getFunctionValue( std::vector< Node >& args ){ return d_tree.getFunctionValue( args, 0, Node::null() ); }
+ /** getFunctionValue for args with set prefix */
+ Node getFunctionValue( const char* argPrefix );
+ /** update
+ * This will update all values in the tree to be representatives in m.
+ */
+ void update( TheoryModel* m ){ d_tree.update( m ); }
/** simplify the tree */
void simplify() { d_tree.simplify( d_op, Node::null(), 0 ); }
/** is this tree total? */
@@ -147,6 +152,7 @@ private:
public:
/** to ITE function for function model nodes */
static Node toIte( Node fm_node, std::vector< Node >& args ) { return toIte2( fm_node, args, 0, Node::null() ); }
+ static Node toIte( TypeNode type, Node fm_node, const char* argPrefix );
};
class UfModelTreeGenerator
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index f0b386cae..47c51d8b9 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -19,10 +19,9 @@
#include "theory/uf/equality_engine.h"
#include "theory/uf/theory_uf_instantiator.h"
#include "theory/theory_engine.h"
-#include "theory/quantifiers/options.h"
#include "theory/quantifiers/term_database.h"
+#include "theory/uf/options.h"
-//#define USE_SMART_SPLITS
//#define ONE_SPLIT_REGION
//#define DISABLE_QUICK_CLIQUE_CHECKS
//#define COMBINE_REGIONS_SMALL_INTO_LARGE
@@ -34,16 +33,11 @@ using namespace CVC4::context;
using namespace CVC4::theory;
using namespace CVC4::theory::uf;
-void StrongSolverTheoryUf::ConflictFind::Region::addRep( Node n ) {
+void StrongSolverTheoryUf::SortRepModel::Region::addRep( Node n ) {
setRep( n, true );
}
-void StrongSolverTheoryUf::ConflictFind::Region::takeNode( StrongSolverTheoryUf::ConflictFind::Region* r, Node n ){
- //Debug("uf-ss") << "takeNode " << r << " " << n << std::endl;
- //Debug("uf-ss") << "r : " << std::endl;
- //r->debugPrint("uf-ss");
- //Debug("uf-ss") << "this : " << std::endl;
- //debugPrint("uf-ss");
+void StrongSolverTheoryUf::SortRepModel::Region::takeNode( StrongSolverTheoryUf::SortRepModel::Region* r, Node n ){
Assert( !hasRep( n ) );
Assert( r->hasRep( n ) );
//add representative
@@ -75,7 +69,7 @@ void StrongSolverTheoryUf::ConflictFind::Region::takeNode( StrongSolverTheoryUf:
r->setRep( n, false );
}
-void StrongSolverTheoryUf::ConflictFind::Region::combine( StrongSolverTheoryUf::ConflictFind::Region* r ){
+void StrongSolverTheoryUf::SortRepModel::Region::combine( StrongSolverTheoryUf::SortRepModel::Region* r ){
//take all nodes from r
for( std::map< Node, RegionNodeInfo* >::iterator it = r->d_nodes.begin(); it != r->d_nodes.end(); ++it ){
if( it->second->d_valid ){
@@ -107,7 +101,7 @@ void StrongSolverTheoryUf::ConflictFind::Region::combine( StrongSolverTheoryUf::
}
/** setEqual */
-void StrongSolverTheoryUf::ConflictFind::Region::setEqual( Node a, Node b ){
+void StrongSolverTheoryUf::SortRepModel::Region::setEqual( Node a, Node b ){
Assert( hasRep( a ) && hasRep( b ) );
//move disequalities of b over to a
for( int t=0; t<2; t++ ){
@@ -129,7 +123,7 @@ void StrongSolverTheoryUf::ConflictFind::Region::setEqual( Node a, Node b ){
setRep( b, false );
}
-void StrongSolverTheoryUf::ConflictFind::Region::setDisequal( Node n1, Node n2, int type, bool valid ){
+void StrongSolverTheoryUf::SortRepModel::Region::setDisequal( Node n1, Node n2, int type, bool valid ){
//Debug("uf-ss-region-debug") << "set disequal " << n1 << " " << n2 << " " << type << " " << valid << std::endl;
//debugPrint("uf-ss-region-debug");
//Assert( isDisequal( n1, n2, type )!=valid );
@@ -155,7 +149,7 @@ void StrongSolverTheoryUf::ConflictFind::Region::setDisequal( Node n1, Node n2,
}
}
-void StrongSolverTheoryUf::ConflictFind::Region::setRep( Node n, bool valid ){
+void StrongSolverTheoryUf::SortRepModel::Region::setRep( Node n, bool valid ){
Assert( hasRep( n )!=valid );
if( valid && d_nodes.find( n )==d_nodes.end() ){
d_nodes[n] = new RegionNodeInfo( d_cf->d_th->getSatContext() );
@@ -179,22 +173,24 @@ void StrongSolverTheoryUf::ConflictFind::Region::setRep( Node n, bool valid ){
}
}
-bool StrongSolverTheoryUf::ConflictFind::Region::isDisequal( Node n1, Node n2, int type ){
+bool StrongSolverTheoryUf::SortRepModel::Region::isDisequal( Node n1, Node n2, int type ){
RegionNodeInfo::DiseqList* del = d_nodes[ n1 ]->d_disequalities[type];
return del->d_disequalities.find( n2 )!=del->d_disequalities.end() && del->d_disequalities[n2];
}
struct sortInternalDegree {
- StrongSolverTheoryUf::ConflictFind::Region* r;
+ StrongSolverTheoryUf::SortRepModel::Region* r;
bool operator() (Node i,Node j) { return (r->d_nodes[i]->getNumInternalDisequalities()>r->d_nodes[j]->getNumInternalDisequalities());}
};
struct sortExternalDegree {
- StrongSolverTheoryUf::ConflictFind::Region* r;
+ StrongSolverTheoryUf::SortRepModel::Region* r;
bool operator() (Node i,Node j) { return (r->d_nodes[i]->getNumExternalDisequalities()>r->d_nodes[j]->getNumExternalDisequalities());}
};
-bool StrongSolverTheoryUf::ConflictFind::Region::getMustCombine( int cardinality ){
+int gmcCount = 0;
+
+bool StrongSolverTheoryUf::SortRepModel::Region::getMustCombine( int cardinality ){
if( options::ufssRegions() && d_total_diseq_external>=long(cardinality) ){
//The number of external disequalities is greater than or equal to cardinality.
//Thus, a clique of size cardinality+1 may exist between nodes in d_regions[i] and other regions
@@ -218,11 +214,10 @@ bool StrongSolverTheoryUf::ConflictFind::Region::getMustCombine( int cardinality
}
}
}
- //static int gmcCount = 0;
- //gmcCount++;
- //if( gmcCount%100==0 ){
- // std::cout << gmcCount << " " << cardinality << std::endl;
- //}
+ gmcCount++;
+ if( gmcCount%100==0 ){
+ Trace("gmc-count") << gmcCount << " " << cardinality << " sample : " << degrees.size() << std::endl;
+ }
//this should happen relatively infrequently....
std::sort( degrees.begin(), degrees.end() );
for( int i=0; i<(int)degrees.size(); i++ ){
@@ -234,16 +229,21 @@ bool StrongSolverTheoryUf::ConflictFind::Region::getMustCombine( int cardinality
return false;
}
-bool StrongSolverTheoryUf::ConflictFind::Region::check( Theory::Effort level, int cardinality, std::vector< Node >& clique ){
+bool StrongSolverTheoryUf::SortRepModel::Region::check( Theory::Effort level, int cardinality, std::vector< Node >& clique ){
if( d_reps_size>long(cardinality) ){
if( d_total_diseq_internal==d_reps_size*( d_reps_size - 1 ) ){
- //quick clique check, all reps form a clique
- for( std::map< Node, RegionNodeInfo* >::iterator it = d_nodes.begin(); it != d_nodes.end(); ++it ){
- if( it->second->d_valid ){
- clique.push_back( it->first );
+ if( d_reps_size>1 ){
+ //quick clique check, all reps form a clique
+ for( std::map< Node, RegionNodeInfo* >::iterator it = d_nodes.begin(); it != d_nodes.end(); ++it ){
+ if( it->second->d_valid ){
+ clique.push_back( it->first );
+ }
}
+ Trace("quick-clique") << "Found quick clique" << std::endl;
+ return true;
+ }else{
+ return false;
}
- return true;
}else if( options::ufssRegions() || options::ufssEagerSplits() || level==Theory::EFFORT_FULL ){
//build test clique, up to size cardinality+1
if( d_testCliqueSize<=long(cardinality) ){
@@ -318,7 +318,7 @@ bool StrongSolverTheoryUf::ConflictFind::Region::check( Theory::Effort level, in
return false;
}
-void StrongSolverTheoryUf::ConflictFind::Region::getRepresentatives( std::vector< Node >& reps ){
+void StrongSolverTheoryUf::SortRepModel::Region::getRepresentatives( std::vector< Node >& reps ){
for( std::map< Node, RegionNodeInfo* >::iterator it = d_nodes.begin(); it != d_nodes.end(); ++it ){
RegionNodeInfo* rni = it->second;
if( rni->d_valid ){
@@ -327,7 +327,7 @@ void StrongSolverTheoryUf::ConflictFind::Region::getRepresentatives( std::vector
}
}
-void StrongSolverTheoryUf::ConflictFind::Region::getNumExternalDisequalities( std::map< Node, int >& num_ext_disequalities ){
+void StrongSolverTheoryUf::SortRepModel::Region::getNumExternalDisequalities( std::map< Node, int >& num_ext_disequalities ){
for( std::map< Node, RegionNodeInfo* >::iterator it = d_nodes.begin(); it != d_nodes.end(); ++it ){
RegionNodeInfo* rni = it->second;
if( rni->d_valid ){
@@ -341,98 +341,7 @@ void StrongSolverTheoryUf::ConflictFind::Region::getNumExternalDisequalities( st
}
}
-Node StrongSolverTheoryUf::ConflictFind::Region::getBestSplit(){
-#ifndef USE_SMART_SPLITS
- //take the first split you find
- for( NodeBoolMap::iterator it = d_splits.begin(); it != d_splits.end(); ++it ){
- if( (*it).second ){
- return (*it).first;
- }
- }
- return Node::null();
-#else
- std::vector< Node > splits;
- for( NodeBoolMap::iterator it = d_splits.begin(); it != d_splits.end(); ++it ){
- if( (*it).second ){
- splits.push_back( (*it).first );
- }
- }
- if( splits.size()>1 ){
- std::map< Node, std::map< Node, bool > > ops;
- Debug("uf-ss-split") << "Choice for splits: " << std::endl;
- double maxScore = -1;
- int maxIndex;
- for( int i=0; i<(int)splits.size(); i++ ){
- Debug("uf-ss-split") << " " << splits[i] << std::endl;
- for( int j=0; j<2; j++ ){
- if( ops.find( splits[i][j] )==ops.end() ){
- EqClassIterator eqc( splits[i][j], ((uf::TheoryUF*)d_cf->d_th)->getEqualityEngine() );
- while( !eqc.isFinished() ){
- Node n = (*eqc);
- if( n.getKind()==APPLY_UF ){
- ops[ splits[i][j] ][ n.getOperator() ] = true;
- }
- ++eqc;
- }
- }
- }
- //now, compute score
- int common[2] = { 0, 0 };
- for( int j=0; j<2; j++ ){
- int j2 = j==0 ? 1 : 0;
- for( std::map< Node, bool >::iterator it = ops[ splits[i][j] ].begin(); it != ops[ splits[i][j] ].end(); ++it ){
- if( ops[ splits[i][j2] ].find( it->first )!=ops[ splits[i][j2] ].end() ){
- common[0]++;
- }else{
- common[1]++;
- }
- }
- }
- double score = ( 1.0 + (double)common[0] )/( 1.0 + (double)common[1] );
- if( score>maxScore ){
- maxScore = score;
- maxIndex = i;
- }
- }
- //if( maxIndex!=0 ){
- // std::cout << "Chose maxIndex = " << maxIndex << std::endl;
- //}
- return splits[maxIndex];
- }else if( !splits.empty() ){
- return splits[0];
- }else{
- return Node::null();
- }
-#endif
-}
-
-void StrongSolverTheoryUf::ConflictFind::Region::addSplit( OutputChannel* out ){
- Node s = getBestSplit();
- //add lemma to output channel
- Assert( s!=Node::null() && s.getKind()==EQUAL );
- s = Rewriter::rewrite( s );
- Debug("uf-ss-lemma") << "*** Split on " << s << std::endl;
- //Debug("uf-ss-lemma") << d_th->getEqualityEngine()->areEqual( s[0], s[1] ) << " ";
- //Debug("uf-ss-lemma") << d_th->getEqualityEngine()->areDisequal( s[0], s[1] ) << std::endl;
- //Debug("uf-ss-lemma") << s[0].getType() << " " << s[1].getType() << std::endl;
- debugPrint("uf-ss-temp");
- //Notice() << "*** Split on " << s << std::endl;
- //split on the equality s
- out->split( s );
- //tell the sat solver to explore the equals branch first
- out->requirePhase( s, true );
-}
-
-bool StrongSolverTheoryUf::ConflictFind::Region::minimize( OutputChannel* out ){
- if( hasSplits() ){
- addSplit( out );
- return false;
- }else{
- return true;
- }
-}
-
-void StrongSolverTheoryUf::ConflictFind::Region::debugPrint( const char* c, bool incClique ){
+void StrongSolverTheoryUf::SortRepModel::Region::debugPrint( const char* c, bool incClique ){
Debug( c ) << "Num reps: " << d_reps_size << std::endl;
for( std::map< Node, RegionNodeInfo* >::iterator it = d_nodes.begin(); it != d_nodes.end(); ++it ){
RegionNodeInfo* rni = it->second;
@@ -474,238 +383,431 @@ void StrongSolverTheoryUf::ConflictFind::Region::debugPrint( const char* c, bool
}
}
-int StrongSolverTheoryUf::ConflictFind::getNumDisequalitiesToRegion( Node n, int ri ){
- int ni = d_regions_map[n];
- int counter = 0;
- Region::RegionNodeInfo::DiseqList* del = d_regions[ni]->d_nodes[n]->d_disequalities[0];
- for( NodeBoolMap::iterator it = del->d_disequalities.begin(); it != del->d_disequalities.end(); ++it ){
- if( (*it).second ){
- if( d_regions_map[ (*it).first ]==ri ){
- counter++;
+
+
+
+
+
+
+
+StrongSolverTheoryUf::SortRepModel::SortRepModel( Node n, context::Context* c, TheoryUF* th ) : RepModel( n.getType() ),
+ d_th( th ), d_regions_index( c, 0 ), d_regions_map( c ), d_split_score( c ), d_disequalities_index( c, 0 ),
+ d_reps( c, 0 ), d_conflict( c, false ), d_cardinality( c, 1 ), d_aloc_cardinality( 0 ),
+ d_cardinality_assertions( c ), d_hasCard( c, false ){
+ d_cardinality_term = n;
+}
+
+/** initialize */
+void StrongSolverTheoryUf::SortRepModel::initialize( OutputChannel* out ){
+ allocateCardinality( out );
+}
+
+/** new node */
+void StrongSolverTheoryUf::SortRepModel::newEqClass( Node n ){
+ if( !d_conflict ){
+ if( d_regions_map.find( n )==d_regions_map.end() ){
+ if( !options::ufssTotalityLazy() ){
+ //must generate totality axioms for every cardinality we have allocated thus far
+ for( std::map< int, Node >::iterator it = d_cardinality_literal.begin(); it != d_cardinality_literal.end(); ++it ){
+ if( applyTotality( it->first ) ){
+ addTotalityAxiom( n, it->first, &d_th->getOutputChannel() );
+ }
+ }
}
+ if( options::ufssTotality() ){
+ //regions map will store whether we need to equate this term with a constant equivalence class
+ if( std::find( d_totality_terms[0].begin(), d_totality_terms[0].end(), n )==d_totality_terms[0].end() ){
+ d_regions_map[n] = 0;
+ }else{
+ d_regions_map[n] = -1;
+ }
+ }else{
+ if( !options::ufssRegions() ){
+ //if not using regions, always add new equivalence classes to region index = 0
+ d_regions_index = 0;
+ }
+ d_regions_map[n] = d_regions_index;
+ if( options::ufssSmartSplits() ){
+ setSplitScore( n, 0 );
+ }
+ Debug("uf-ss") << "StrongSolverTheoryUf: New Eq Class " << n << std::endl;
+ Debug("uf-ss-debug") << d_regions_index << " " << (int)d_regions.size() << std::endl;
+ if( d_regions_index<d_regions.size() ){
+ d_regions[ d_regions_index ]->debugPrint("uf-ss-debug",true);
+ d_regions[ d_regions_index ]->d_valid = true;
+ Assert( !options::ufssRegions() || d_regions[ d_regions_index ]->getNumReps()==0 );
+ }else{
+ d_regions.push_back( new Region( this, d_th->getSatContext() ) );
+ }
+ d_regions[ d_regions_index ]->addRep( n );
+ d_regions_index = d_regions_index + 1;
+ }
+ d_reps = d_reps + 1;
}
}
- return counter;
}
-void StrongSolverTheoryUf::ConflictFind::getDisequalitiesToRegions( int ri, std::map< int, int >& regions_diseq ){
- for( std::map< Node, Region::RegionNodeInfo* >::iterator it = d_regions[ri]->d_nodes.begin();
- it != d_regions[ri]->d_nodes.end(); ++it ){
- if( it->second->d_valid ){
- Region::RegionNodeInfo::DiseqList* del = it->second->d_disequalities[0];
- for( NodeBoolMap::iterator it2 = del->d_disequalities.begin(); it2 != del->d_disequalities.end(); ++it2 ){
- if( (*it2).second ){
- Assert( isValid( d_regions_map[ (*it2).first ] ) );
- //Notice() << "Found disequality with " << (*it2).first << ", region = " << d_regions_map[ (*it2).first ] << std::endl;
- regions_diseq[ d_regions_map[ (*it2).first ] ]++;
+/** merge */
+void StrongSolverTheoryUf::SortRepModel::merge( Node a, Node b ){
+ if( !d_conflict ){
+ if( options::ufssTotality() ){
+ if( d_regions_map[b]==-1 ){
+ d_regions_map[a] = -1;
+ }
+ d_regions_map[b] = -1;
+ }else{
+ //Assert( a==d_th->d_equalityEngine.getRepresentative( a ) );
+ //Assert( b==d_th->d_equalityEngine.getRepresentative( b ) );
+ Debug("uf-ss") << "StrongSolverTheoryUf: Merging " << a << " = " << b << "..." << std::endl;
+ if( a!=b ){
+ Assert( d_regions_map.find( a )!=d_regions_map.end() );
+ Assert( d_regions_map.find( b )!=d_regions_map.end() );
+ int ai = d_regions_map[a];
+ int bi = d_regions_map[b];
+ Debug("uf-ss") << " regions: " << ai << " " << bi << std::endl;
+ if( ai!=bi ){
+ if( d_regions[ai]->getNumReps()==1 ){
+ int ri = combineRegions( bi, ai );
+ d_regions[ri]->setEqual( a, b );
+ checkRegion( ri );
+ }else if( d_regions[bi]->getNumReps()==1 ){
+ int ri = combineRegions( ai, bi );
+ d_regions[ri]->setEqual( a, b );
+ checkRegion( ri );
+ }else{
+ // either move a to d_regions[bi], or b to d_regions[ai]
+ int aex = d_regions[ai]->d_nodes[a]->getNumInternalDisequalities() - getNumDisequalitiesToRegion( a, bi );
+ int bex = d_regions[bi]->d_nodes[b]->getNumInternalDisequalities() - getNumDisequalitiesToRegion( b, ai );
+ //based on which would produce the fewest number of external disequalities
+ if( aex<bex ){
+ moveNode( a, bi );
+ d_regions[bi]->setEqual( a, b );
+ }else{
+ moveNode( b, ai );
+ d_regions[ai]->setEqual( a, b );
+ }
+ checkRegion( ai );
+ checkRegion( bi );
+ }
+ }else{
+ d_regions[ai]->setEqual( a, b );
+ checkRegion( ai );
}
+ d_regions_map[b] = -1;
}
+ d_reps = d_reps - 1;
+ Debug("uf-ss") << "Done merge." << std::endl;
}
}
}
-void StrongSolverTheoryUf::ConflictFind::explainClique( std::vector< Node >& clique, OutputChannel* out ){
- Assert( d_cardinality>0 );
- while( clique.size()>size_t(d_cardinality+1) ){
- clique.pop_back();
- }
- //found a clique
- Debug("uf-ss") << "Found a clique (cardinality=" << d_cardinality << ") :" << std::endl;
- Debug("uf-ss") << " ";
- for( int i=0; i<(int)clique.size(); i++ ){
- Debug("uf-ss") << clique[i] << " ";
- }
- Debug("uf-ss") << std::endl;
- Debug("uf-ss") << "Finding clique disequalities..." << std::endl;
- std::vector< Node > conflict;
- //collect disequalities, and nodes that must be equal within representatives
- std::map< Node, std::map< Node, bool > > explained;
- std::map< Node, std::map< Node, bool > > nodesWithinRep;
- for( int i=0; i<(int)d_disequalities_index; i++ ){
- //if both sides of disequality exist in clique
- Node r1 = d_th->d_equalityEngine.getRepresentative( d_disequalities[i][0][0] );
- Node r2 = d_th->d_equalityEngine.getRepresentative( d_disequalities[i][0][1] );
- if( r1!=r2 && ( explained.find( r1 )==explained.end() || explained[r1].find( r2 )==explained[r1].end() ) &&
- std::find( clique.begin(), clique.end(), r1 )!=clique.end() &&
- std::find( clique.begin(), clique.end(), r2 )!=clique.end() ){
- explained[r1][r2] = true;
- explained[r2][r1] = true;
- conflict.push_back( d_disequalities[i] );
- nodesWithinRep[r1][ d_disequalities[i][0][0] ] = true;
- nodesWithinRep[r2][ d_disequalities[i][0][1] ] = true;
- if( conflict.size()==(clique.size()*( clique.size()-1 )/2) ){
- break;
+/** assert terms are disequal */
+void StrongSolverTheoryUf::SortRepModel::assertDisequal( Node a, Node b, Node reason ){
+ if( !d_conflict ){
+ if( options::ufssTotality() ){
+ //do nothing
+ }else{
+ //if they are not already disequal
+ a = d_th->d_equalityEngine.getRepresentative( a );
+ b = d_th->d_equalityEngine.getRepresentative( b );
+ if( !d_th->d_equalityEngine.areDisequal( a, b, true ) ){
+ Debug("uf-ss") << "Assert disequal " << a << " != " << b << "..." << std::endl;
+ //if( reason.getKind()!=NOT || ( reason[0].getKind()!=EQUAL && reason[0].getKind()!=IFF ) ||
+ // a!=reason[0][0] || b!=reason[0][1] ){
+ // Notice() << "Assert disequal " << a << " != " << b << ", reason = " << reason << "..." << std::endl;
+ //}
+ Debug("uf-ss-disequal") << "Assert disequal " << a << " != " << b << "..." << std::endl;
+ //add to list of disequalities
+ if( d_disequalities_index<d_disequalities.size() ){
+ d_disequalities[d_disequalities_index] = reason;
+ }else{
+ d_disequalities.push_back( reason );
+ }
+ d_disequalities_index = d_disequalities_index + 1;
+ //now, add disequalities to regions
+ Assert( d_regions_map.find( a )!=d_regions_map.end() );
+ Assert( d_regions_map.find( b )!=d_regions_map.end() );
+ int ai = d_regions_map[a];
+ int bi = d_regions_map[b];
+ Debug("uf-ss") << " regions: " << ai << " " << bi << std::endl;
+ if( ai==bi ){
+ //internal disequality
+ d_regions[ai]->setDisequal( a, b, 1, true );
+ d_regions[ai]->setDisequal( b, a, 1, true );
+ }else{
+ //external disequality
+ d_regions[ai]->setDisequal( a, b, 0, true );
+ d_regions[bi]->setDisequal( b, a, 0, true );
+ checkRegion( ai );
+ checkRegion( bi );
+ }
+ //Notice() << "done" << std::endl;
}
}
}
- //Debug("uf-ss") << conflict.size() << " " << clique.size() << std::endl;
- Assert( (int)conflict.size()==((int)clique.size()*( (int)clique.size()-1 )/2) );
- //Assert( (int)conflict.size()==(int)clique.size()*( (int)clique.size()-1 )/2 );
- Debug("uf-ss") << "Finding clique equalities internal to eq classes..." << std::endl;
- //now, we must explain equalities within each equivalence class
- for( std::map< Node, std::map< Node, bool > >::iterator it = nodesWithinRep.begin(); it != nodesWithinRep.end(); ++it ){
- if( it->second.size()>1 ){
- Node prev;
- //add explanation of t1 = t2 = ... = tn
- for( std::map< Node, bool >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
- if( prev!=Node::null() ){
- //explain it2->first and prev
- std::vector< TNode > expl;
- d_th->d_equalityEngine.explainEquality( it2->first, prev, true, expl );
- for( int i=0; i<(int)expl.size(); i++ ){
- if( std::find( conflict.begin(), conflict.end(), expl[i] )==conflict.end() ){
- conflict.push_back( expl[i] );
+}
+
+
+/** check */
+void StrongSolverTheoryUf::SortRepModel::check( Theory::Effort level, OutputChannel* out ){
+ if( level>=Theory::EFFORT_STANDARD && d_hasCard && !d_conflict ){
+ Debug("uf-ss") << "StrongSolverTheoryUf: Check " << level << " " << d_type << std::endl;
+ //Notice() << "StrongSolverTheoryUf: Check " << level << std::endl;
+ if( d_reps<=(unsigned)d_cardinality ){
+ Debug("uf-ss-debug") << "We have " << d_reps << " representatives for type " << d_type << ", <= " << d_cardinality << std::endl;
+ if( level==Theory::EFFORT_FULL ){
+ Debug("uf-ss-sat") << "We have " << d_reps << " representatives for type " << d_type << ", <= " << d_cardinality << std::endl;
+ //Notice() << "We have " << d_reps << " representatives for type " << d_type << ", <= " << cardinality << std::endl;
+ //Notice() << "Model size for " << d_type << " is " << cardinality << std::endl;
+ //Notice() << cardinality << " ";
+ }
+ return;
+ }else{
+ if( applyTotality( d_cardinality ) ){
+ //if we are applying totality to this cardinality
+ if( options::ufssTotalityLazy() ){
+ //add totality axioms for all nodes that have not yet been equated to cardinality terms
+ if( level==Theory::EFFORT_FULL ){
+ for( NodeIntMap::iterator it = d_regions_map.begin(); it != d_regions_map.end(); ++it ){
+ if( !options::ufssTotality() || d_regions_map[ (*it).first ]!=-1 ){
+ addTotalityAxiom( (*it).first, d_cardinality, &d_th->getOutputChannel() );
+ }
+ }
+ }
+ }
+ }else{
+ //do a check within each region
+ for( int i=0; i<(int)d_regions_index; i++ ){
+ if( d_regions[i]->d_valid ){
+ std::vector< Node > clique;
+ if( d_regions[i]->check( level, d_cardinality, clique ) ){
+ //add clique lemma
+ addCliqueLemma( clique, out );
+ return;
+ }else{
+ Trace("uf-ss-debug") << "No clique in Region #" << i << std::endl;
+ }
+ }
+ }
+ bool addedLemma = false;
+ //do splitting on demand
+ if( level==Theory::EFFORT_FULL || options::ufssEagerSplits() ){
+ Trace("uf-ss-debug") << "Add splits?" << std::endl;
+ //see if we have any recommended splits from large regions
+ for( int i=0; i<(int)d_regions_index; i++ ){
+ if( d_regions[i]->d_valid && d_regions[i]->getNumReps()>d_cardinality ){
+ if( addSplit( d_regions[i], out ) ){
+ addedLemma = true;
+#ifdef ONE_SPLIT_REGION
+ break;
+#endif
+ }
+ }
+ }
+ }
+ //if no added lemmas, force continuation via combination of regions
+ if( level==Theory::EFFORT_FULL ){
+ if( !addedLemma ){
+ Trace("uf-ss-debug") << "No splits added. " << d_cardinality << std::endl;
+ if( !options::ufssColoringSat() ){
+ bool recheck = false;
+ //naive strategy, force region combination involving the first valid region
+ for( int i=0; i<(int)d_regions_index; i++ ){
+ if( d_regions[i]->d_valid ){
+ forceCombineRegion( i, false );
+ recheck = true;
+ break;
+ }
+ }
+ if( recheck ){
+ check( level, out );
+ }
}
}
}
- prev = it2->first;
}
}
}
- Debug("uf-ss") << "Explanation of clique (size=" << conflict.size() << ") = " << std::endl;
- for( int i=0; i<(int)conflict.size(); i++ ){
- Debug("uf-ss") << conflict[i] << " ";
- }
- Debug("uf-ss") << std::endl;
- //now, make the conflict
- Node conflictNode = conflict.size()==1 ? conflict[0] : NodeManager::currentNM()->mkNode( AND, conflict );
- //add cardinality constraint
- //Node cardNode = NodeManager::currentNM()->mkNode( CARDINALITY_CONSTRAINT, d_cardinality_lemma_term,
- // NodeManager::currentNM()->mkConst( Rational(d_cardinality) ) );
- Node cardNode = d_cardinality_literal[ d_cardinality ];
- conflictNode = NodeManager::currentNM()->mkNode( IMPLIES, conflictNode, cardNode.notNode() );
- Debug("uf-ss-lemma") << "*** Add clique conflict " << conflictNode << std::endl;
- //Notice() << "*** Add clique conflict " << conflictNode << std::endl;
- out->lemma( conflictNode );
- ++( d_th->getStrongSolver()->d_statistics.d_clique_lemmas );
+}
+
+void StrongSolverTheoryUf::SortRepModel::propagate( Theory::Effort level, OutputChannel* out ){
- //DO_THIS: ensure that the same clique is not reported??? Check standard effort after assertDisequal can produce same clique.
}
-/** new node */
-void StrongSolverTheoryUf::ConflictFind::newEqClass( Node n ){
- if( d_regions_map.find( n )==d_regions_map.end() ){
- if( !options::ufssRegions() ){
- //if not using regions, always add new equivalence classes to region index = 0
- d_regions_index = 0;
- }
- d_regions_map[n] = d_regions_index;
- Debug("uf-ss") << "StrongSolverTheoryUf: New Eq Class " << n << std::endl;
- Debug("uf-ss-debug") << d_regions_index << " " << (int)d_regions.size() << std::endl;
- if( d_regions_index<d_regions.size() ){
- d_regions[ d_regions_index ]->debugPrint("uf-ss-debug",true);
- d_regions[ d_regions_index ]->d_valid = true;
- Assert( !options::ufssRegions() || d_regions[ d_regions_index ]->getNumReps()==0 );
- }else{
- d_regions.push_back( new Region( this, d_th->getSatContext() ) );
+Node StrongSolverTheoryUf::SortRepModel::getNextDecisionRequest(){
+ //request the current cardinality as a decision literal, if not already asserted
+ for( int i=1; i<=d_aloc_cardinality; i++ ){
+ if( !d_hasCard || i<d_cardinality ){
+ Node cn = d_cardinality_literal[ i ];
+ Assert( !cn.isNull() );
+ if( d_cardinality_assertions.find( cn )==d_cardinality_assertions.end() ){
+ Trace("uf-ss-dec") << "Propagate as decision " << d_type << " " << i << std::endl;
+ return cn;
+ }
}
- d_regions[ d_regions_index ]->addRep( n );
- d_regions_index = d_regions_index + 1;
- d_reps = d_reps + 1;
}
+ return Node::null();
}
-/** merge */
-void StrongSolverTheoryUf::ConflictFind::merge( Node a, Node b ){
- //Assert( a==d_th->d_equalityEngine.getRepresentative( a ) );
- //Assert( b==d_th->d_equalityEngine.getRepresentative( b ) );
- Debug("uf-ss") << "StrongSolverTheoryUf: Merging " << a << " = " << b << "..." << std::endl;
- if( a!=b ){
- Assert( d_regions_map.find( a )!=d_regions_map.end() );
- Assert( d_regions_map.find( b )!=d_regions_map.end() );
- int ai = d_regions_map[a];
- int bi = d_regions_map[b];
- Debug("uf-ss") << " regions: " << ai << " " << bi << std::endl;
- if( ai!=bi ){
- if( d_regions[ai]->getNumReps()==1 ){
- int ri = combineRegions( bi, ai );
- d_regions[ri]->setEqual( a, b );
- checkRegion( ri );
- }else if( d_regions[bi]->getNumReps()==1 ){
- int ri = combineRegions( ai, bi );
- d_regions[ri]->setEqual( a, b );
- checkRegion( ri );
- }else{
- // either move a to d_regions[bi], or b to d_regions[ai]
- int aex = d_regions[ai]->d_nodes[a]->getNumInternalDisequalities() - getNumDisequalitiesToRegion( a, bi );
- int bex = d_regions[bi]->d_nodes[b]->getNumInternalDisequalities() - getNumDisequalitiesToRegion( b, ai );
- //based on which would produce the fewest number of external disequalities
- if( aex<bex ){
- moveNode( a, bi );
- d_regions[bi]->setEqual( a, b );
- }else{
- moveNode( b, ai );
- d_regions[ai]->setEqual( a, b );
+bool StrongSolverTheoryUf::SortRepModel::minimize( OutputChannel* out, TheoryModel* m ){
+ if( options::ufssTotality() ){
+ //do nothing
+ }else{
+ if( m ){
+#if 0
+ // ensure that the constructed model is minimal
+ // if the model has terms that the strong solver does not know about
+ if( (int)m->d_rep_set.d_type_reps[ d_type ].size()>d_cardinality ){
+ eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &m->d_equalityEngine );
+ while( !eqcs_i.isFinished() ){
+ Node eqc = (*eqcs_i);
+ if( eqc.getType()==d_type ){
+ //we must ensure that this equivalence class has been accounted for
+ if( d_regions_map.find( eqc )==d_regions_map.end() ){
+ //split on unaccounted for term and cardinality lemma term (as default)
+ Node splitEq = eqc.eqNode( d_cardinality_term );
+ splitEq = Rewriter::rewrite( splitEq );
+ Trace("uf-ss-minimize") << "Last chance minimize : " << splitEq << std::endl;
+ out->split( splitEq );
+ //tell the sat solver to explore the equals branch first
+ out->requirePhase( splitEq, true );
+ ++( d_th->getStrongSolver()->d_statistics.d_split_lemmas );
+ return false;
+ }
+ }
+ ++eqcs_i;
}
- checkRegion( ai );
- checkRegion( bi );
+ Assert( false );
}
+#endif
}else{
- d_regions[ai]->setEqual( a, b );
- checkRegion( ai );
+ //internal minimize, ensure that model forms a clique:
+ // if two equivalence classes are neither equal nor disequal, add a split
+ int validRegionIndex = -1;
+ for( int i=0; i<(int)d_regions_index; i++ ){
+ if( d_regions[i]->d_valid ){
+ if( validRegionIndex!=-1 ){
+ combineRegions( validRegionIndex, i );
+ if( addSplit( d_regions[validRegionIndex], out ) ){
+ return false;
+ }
+ }else{
+ validRegionIndex = i;
+ }
+ }
+ }
+ if( addSplit( d_regions[validRegionIndex], out ) ){
+ return false;
+ }
}
- d_reps = d_reps - 1;
- d_regions_map[b] = -1;
}
- Debug("uf-ss") << "Done merge." << std::endl;
+ return true;
}
-/** assert terms are disequal */
-void StrongSolverTheoryUf::ConflictFind::assertDisequal( Node a, Node b, Node reason ){
- //if they are not already disequal
- a = d_th->d_equalityEngine.getRepresentative( a );
- b = d_th->d_equalityEngine.getRepresentative( b );
- if( !d_th->d_equalityEngine.areDisequal( a, b, true ) ){
- Debug("uf-ss") << "Assert disequal " << a << " != " << b << "..." << std::endl;
- //if( reason.getKind()!=NOT || ( reason[0].getKind()!=EQUAL && reason[0].getKind()!=IFF ) ||
- // a!=reason[0][0] || b!=reason[0][1] ){
- // Notice() << "Assert disequal " << a << " != " << b << ", reason = " << reason << "..." << std::endl;
- //}
- Debug("uf-ss-disequal") << "Assert disequal " << a << " != " << b << "..." << std::endl;
- //add to list of disequalities
- if( d_disequalities_index<d_disequalities.size() ){
- d_disequalities[d_disequalities_index] = reason;
- }else{
- d_disequalities.push_back( reason );
+
+int StrongSolverTheoryUf::SortRepModel::getNumDisequalitiesToRegion( Node n, int ri ){
+ int ni = d_regions_map[n];
+ int counter = 0;
+ Region::RegionNodeInfo::DiseqList* del = d_regions[ni]->d_nodes[n]->d_disequalities[0];
+ for( NodeBoolMap::iterator it = del->d_disequalities.begin(); it != del->d_disequalities.end(); ++it ){
+ if( (*it).second ){
+ if( d_regions_map[ (*it).first ]==ri ){
+ counter++;
+ }
}
- d_disequalities_index = d_disequalities_index + 1;
- //now, add disequalities to regions
- Assert( d_regions_map.find( a )!=d_regions_map.end() );
- Assert( d_regions_map.find( b )!=d_regions_map.end() );
- int ai = d_regions_map[a];
- int bi = d_regions_map[b];
- Debug("uf-ss") << " regions: " << ai << " " << bi << std::endl;
- if( ai==bi ){
- //internal disequality
- d_regions[ai]->setDisequal( a, b, 1, true );
- d_regions[ai]->setDisequal( b, a, 1, true );
- }else{
- //external disequality
- d_regions[ai]->setDisequal( a, b, 0, true );
- d_regions[bi]->setDisequal( b, a, 0, true );
- checkRegion( ai );
- checkRegion( bi );
+ }
+ return counter;
+}
+
+void StrongSolverTheoryUf::SortRepModel::getDisequalitiesToRegions( int ri, std::map< int, int >& regions_diseq ){
+ for( std::map< Node, Region::RegionNodeInfo* >::iterator it = d_regions[ri]->d_nodes.begin();
+ it != d_regions[ri]->d_nodes.end(); ++it ){
+ if( it->second->d_valid ){
+ Region::RegionNodeInfo::DiseqList* del = it->second->d_disequalities[0];
+ for( NodeBoolMap::iterator it2 = del->d_disequalities.begin(); it2 != del->d_disequalities.end(); ++it2 ){
+ if( (*it2).second ){
+ Assert( isValid( d_regions_map[ (*it2).first ] ) );
+ //Notice() << "Found disequality with " << (*it2).first << ", region = " << d_regions_map[ (*it2).first ] << std::endl;
+ regions_diseq[ d_regions_map[ (*it2).first ] ]++;
+ }
+ }
}
- //Notice() << "done" << std::endl;
}
}
-void StrongSolverTheoryUf::ConflictFind::assertCardinality( int c, bool val ){
- Assert( d_cardinality_literal.find( c )!=d_cardinality_literal.end() );
- d_cardinality_assertions[ d_cardinality_literal[c] ] = val;
- if( val ){
- d_hasCard = true;
+void StrongSolverTheoryUf::SortRepModel::setSplitScore( Node n, int s ){
+ if( d_split_score.find( n )!=d_split_score.end() ){
+ int ss = d_split_score[ n ];
+ d_split_score[ n ] = s>ss ? s : ss;
+ }else{
+ d_split_score[ n ] = s;
+ }
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ setSplitScore( n[i], s+1 );
+ }
+}
+
+void StrongSolverTheoryUf::SortRepModel::assertCardinality( OutputChannel* out, int c, bool val ){
+ if( !d_conflict ){
+ Trace("uf-ss-assert") << "Assert cardinality " << d_type << " " << c << " " << val << " level = " << d_th->d_valuation.getAssertionLevel() << std::endl;
+ Assert( d_cardinality_literal.find( c )!=d_cardinality_literal.end() );
+ d_cardinality_assertions[ d_cardinality_literal[c] ] = val;
+ if( val ){
+ bool doCheckRegions = !d_hasCard;
+ if( !d_hasCard || c<d_cardinality ){
+ d_cardinality = c;
+ }
+ d_hasCard = true;
+ //should check all regions now
+ if( doCheckRegions ){
+ for( int i=0; i<(int)d_regions_index; i++ ){
+ if( d_regions[i]->d_valid ){
+ checkRegion( i );
+ if( d_conflict ){
+ return;
+ }
+ }
+ }
+ }
+ }else{
+ if( options::ufssModelInference() ){
+ //check if we are at decision level 0
+ if( d_th->d_valuation.getAssertionLevel()==0 ){
+ Trace("uf-ss-mi") << "We have proved that no models of size " << c << " for type " << d_type << " exist." << std::endl;
+ Trace("uf-ss-mi") << " # Clique lemmas : " << d_cliques[c].size() << std::endl;
+ if( d_cliques[c].size()==1 ){
+ if( d_totality_terms[c+1].empty() ){
+ Trace("uf-ss-mi") << "*** Establish model" << std::endl;
+ //d_totality_terms[c+1].insert( d_totality_terms[c].begin(), d_cliques[c][0].begin(), d_cliques[c][0].end() );
+ }
+ }
+ }
+ }
+ //see if we need to request a new cardinality
+ if( !d_hasCard ){
+ bool needsCard = true;
+ for( std::map< int, Node >::iterator it = d_cardinality_literal.begin(); it!=d_cardinality_literal.end(); ++it ){
+ if( d_cardinality_assertions.find( it->second )==d_cardinality_assertions.end() ){
+ needsCard = false;
+ break;
+ }
+ }
+ if( needsCard ){
+ allocateCardinality( out );
+ }
+ }
+ }
}
}
-void StrongSolverTheoryUf::ConflictFind::checkRegion( int ri, bool rec ){
- if( isValid(ri) ){
+void StrongSolverTheoryUf::SortRepModel::checkRegion( int ri, bool rec ){
+ if( isValid(ri) && d_hasCard ){
Assert( d_cardinality>0 );
//first check if region is in conflict
std::vector< Node > clique;
if( d_regions[ri]->check( Theory::EFFORT_STANDARD, d_cardinality, clique ) ){
//explain clique
- explainClique( clique, &d_th->getOutputChannel() );
+ addCliqueLemma( clique, &d_th->getOutputChannel() );
}else if( d_regions[ri]->getMustCombine( d_cardinality ) ){
////alternatively, check if we can reduce the number of external disequalities by moving single nodes
//for( std::map< Node, bool >::iterator it = d_regions[i]->d_reps.begin(); it != d_regions[i]->d_reps.end(); ++it ){
@@ -724,7 +826,7 @@ void StrongSolverTheoryUf::ConflictFind::checkRegion( int ri, bool rec ){
}
}
-int StrongSolverTheoryUf::ConflictFind::forceCombineRegion( int ri, bool useDensity ){
+int StrongSolverTheoryUf::SortRepModel::forceCombineRegion( int ri, bool useDensity ){
if( !useDensity ){
for( int i=0; i<(int)d_regions_index; i++ ){
if( ri!=i && d_regions[i]->d_valid ){
@@ -764,7 +866,7 @@ int StrongSolverTheoryUf::ConflictFind::forceCombineRegion( int ri, bool useDens
}
-int StrongSolverTheoryUf::ConflictFind::combineRegions( int ai, int bi ){
+int StrongSolverTheoryUf::SortRepModel::combineRegions( int ai, int bi ){
#ifdef COMBINE_REGIONS_SMALL_INTO_LARGE
if( d_regions[ai]->getNumReps()<d_regions[bi]->getNumReps() ){
return combineRegions( bi, ai );
@@ -784,7 +886,7 @@ int StrongSolverTheoryUf::ConflictFind::combineRegions( int ai, int bi ){
return ai;
}
-void StrongSolverTheoryUf::ConflictFind::moveNode( Node n, int ri ){
+void StrongSolverTheoryUf::SortRepModel::moveNode( Node n, int ri ){
Debug("uf-ss-region") << "uf-ss: Move node " << n << " to Region #" << ri << std::endl;
Assert( isValid( d_regions_map[ n ] ) );
Assert( isValid( ri ) );
@@ -793,161 +895,248 @@ void StrongSolverTheoryUf::ConflictFind::moveNode( Node n, int ri ){
d_regions_map[n] = ri;
}
-bool StrongSolverTheoryUf::ConflictFind::disambiguateTerms( OutputChannel* out ){
- Debug("uf-ss-disamb") << "Disambiguate terms." << std::endl;
- bool lemmaAdded = false;
- //otherwise, determine ambiguous pairs of ground terms for relevant sorts
- quantifiers::TermDb* db = d_th->getQuantifiersEngine()->getTermDatabase();
- for( std::map< Node, std::vector< Node > >::iterator it = db->d_op_map.begin(); it != db->d_op_map.end(); ++it ){
- Debug("uf-ss-disamb") << "Check " << it->first << std::endl;
- if( it->second.size()>1 ){
- if( StrongSolverTheoryUf::involvesRelevantType( it->second[0] ) ){
- for( int i=0; i<(int)it->second.size(); i++ ){
- for( int j=(i+1); j<(int)it->second.size(); j++ ){
- Kind knd = it->second[i].getType()==NodeManager::currentNM()->booleanType() ? IFF : EQUAL;
- Node eq = NodeManager::currentNM()->mkNode( knd, it->second[i], it->second[j] );
- eq = Rewriter::rewrite(eq);
- //determine if they are ambiguous
- if( d_term_amb.find( eq )==d_term_amb.end() ){
- Debug("uf-ss-disamb") << "Check disambiguate " << it->second[i] << " " << it->second[j] << std::endl;
- d_term_amb[ eq ] = true;
- //if they are equal
- if( d_th->d_equalityEngine.areEqual( it->second[i], it->second[j] ) ){
- d_term_amb[ eq ] = false;
- }else{
- //if an argument is disequal, then they are not ambiguous
- for( int k=0; k<(int)it->second[i].getNumChildren(); k++ ){
- if( d_th->d_equalityEngine.areDisequal( it->second[i][k], it->second[j][k], true ) ){
- d_term_amb[ eq ] = false;
- break;
- }
- }
- }
- if( d_term_amb[ eq ] ){
- Debug("uf-ss-disamb") << "Disambiguate " << it->second[i] << " " << it->second[j] << std::endl;
- //must add lemma
- std::vector< Node > children;
- children.push_back( eq );
- for( int k=0; k<(int)it->second[i].getNumChildren(); k++ ){
- Kind knd2 = it->second[i][k].getType()==NodeManager::currentNM()->booleanType() ? IFF : EQUAL;
- Node eqc = NodeManager::currentNM()->mkNode( knd2, it->second[i][k], it->second[j][k] );
- children.push_back( eqc.notNode() );
- }
- Assert( children.size()>1 );
- Node lem = NodeManager::currentNM()->mkNode( OR, children );
- Debug( "uf-ss-lemma" ) << "*** Disambiguate lemma : " << lem << std::endl;
- //Notice() << "*** Disambiguate lemma : " << lem << std::endl;
- out->lemma( lem );
- d_term_amb[ eq ] = false;
- lemmaAdded = true;
- ++( d_th->getStrongSolver()->d_statistics.d_disamb_term_lemmas );
- }
- }
- }
+void StrongSolverTheoryUf::SortRepModel::allocateCardinality( OutputChannel* out ){
+ if( d_aloc_cardinality>0 ){
+ Trace("uf-ss-fmf") << "No model of size " << d_aloc_cardinality << " exists for type " << d_type << " in this branch" << std::endl;
+ if( Trace.isOn("uf-ss-cliques") ){
+ Trace("uf-ss-cliques") << "Cliques of size " << (d_aloc_cardinality+1) << " : " << std::endl;
+ for( size_t i=0; i<d_cliques[ d_aloc_cardinality ].size(); i++ ){
+ Trace("uf-ss-cliques") << " ";
+ for( size_t j=0; j<d_cliques[ d_aloc_cardinality ][i].size(); j++ ){
+ Trace("uf-ss-cliques") << d_cliques[ d_aloc_cardinality ][i][j] << " ";
}
+ Trace("uf-ss-cliques") << std::endl;
+ }
+ }
+ }
+ d_aloc_cardinality++;
+
+ //check for abort case
+ if( options::ufssAbortCardinality()==d_aloc_cardinality ){
+ //abort here DO_THIS
+ Message() << "Maximum cardinality reached." << std::endl;
+ exit( 0 );
+ }else{
+ if( options::ufssTotality() ){
+ //must generate new cardinality lemma term
+ std::stringstream ss;
+ ss << "_c_" << d_aloc_cardinality;
+ Node var = NodeManager::currentNM()->mkSkolem( ss.str(), d_type );
+ d_totality_terms[0].push_back( var );
+ Trace("mkVar") << "allocateCardinality, mkVar : " << var << " : " << d_type << std::endl;
+ //must be distinct from all other cardinality terms
+ for( int i=0; i<(int)(d_totality_terms[0].size()-1); i++ ){
+ Node lem = NodeManager::currentNM()->mkNode( NOT, var.eqNode( d_totality_terms[0][i] ) );
+ d_th->getOutputChannel().lemma( lem );
+ }
+ }
+
+ //add splitting lemma for cardinality constraint
+ Assert( !d_cardinality_term.isNull() );
+ Node lem = NodeManager::currentNM()->mkNode( CARDINALITY_CONSTRAINT, d_cardinality_term,
+ NodeManager::currentNM()->mkConst( Rational( d_aloc_cardinality ) ) );
+ lem = Rewriter::rewrite(lem);
+ d_cardinality_literal[ d_aloc_cardinality ] = lem;
+ lem = NodeManager::currentNM()->mkNode( OR, lem, lem.notNode() );
+ d_cardinality_lemma[ d_aloc_cardinality ] = lem;
+ //add as lemma to output channel
+ out->lemma( lem );
+ //require phase
+ out->requirePhase( d_cardinality_literal[ d_aloc_cardinality ], true );
+ //add the appropriate lemma, propagate as decision
+ //Trace("uf-ss-prop-as-dec") << "Propagate as decision " << lem[0] << " " << d_type << std::endl;
+ //out->propagateAsDecision( lem[0] );
+ d_th->getStrongSolver()->d_statistics.d_max_model_size.maxAssign( d_aloc_cardinality );
+
+ if( applyTotality( d_aloc_cardinality ) && !options::ufssTotalityLazy() ){
+ //must send totality axioms for each existing term
+ for( NodeIntMap::iterator it = d_regions_map.begin(); it != d_regions_map.end(); ++it ){
+ addTotalityAxiom( (*it).first, d_aloc_cardinality, &d_th->getOutputChannel() );
}
}
}
- Debug("uf-ss-disamb") << "Done disambiguate terms. " << lemmaAdded << std::endl;
- return lemmaAdded;
}
-/** check */
-void StrongSolverTheoryUf::ConflictFind::check( Theory::Effort level, OutputChannel* out ){
- if( level>=Theory::EFFORT_STANDARD ){
- Assert( d_cardinality>0 );
- Debug("uf-ss") << "StrongSolverTheoryUf: Check " << level << " " << d_type << std::endl;
- //Notice() << "StrongSolverTheoryUf: Check " << level << std::endl;
- if( d_reps<=(unsigned)d_cardinality ){
- Debug("uf-ss-debug") << "We have " << d_reps << " representatives for type " << d_type << ", <= " << d_cardinality << std::endl;
- if( level==Theory::EFFORT_FULL ){
- Debug("uf-ss-sat") << "We have " << d_reps << " representatives for type " << d_type << ", <= " << d_cardinality << std::endl;
- //Notice() << "We have " << d_reps << " representatives for type " << d_type << ", <= " << cardinality << std::endl;
- //Notice() << "Model size for " << d_type << " is " << cardinality << std::endl;
- //Notice() << cardinality << " ";
+bool StrongSolverTheoryUf::SortRepModel::addSplit( Region* r, OutputChannel* out ){
+ if( r->hasSplits() ){
+ Node s;
+ if( !options::ufssSmartSplits() ){
+ //take the first split you find
+ for( NodeBoolMap::iterator it = r->d_splits.begin(); it != r->d_splits.end(); ++it ){
+ if( (*it).second ){
+ s = (*it).first;
+ break;
+ }
}
- return;
}else{
- //do a check within each region
- for( int i=0; i<(int)d_regions_index; i++ ){
- if( d_regions[i]->d_valid ){
- std::vector< Node > clique;
- if( d_regions[i]->check( level, d_cardinality, clique ) ){
- //explain clique
- explainClique( clique, out );
- return;
- }else{
- Debug("uf-ss-debug") << "No clique in Region #" << i << std::endl;
+ int maxScore = -1;
+ std::vector< Node > splits;
+ for( NodeBoolMap::iterator it = r->d_splits.begin(); it != r->d_splits.end(); ++it ){
+ if( (*it).second ){
+ int score1 = d_split_score[ (*it).first[0] ];
+ int score2 = d_split_score[ (*it).first[1] ];
+ int score = score1<score2 ? score1 : score2;
+ if( score>maxScore ){
+ maxScore = -1;
+ s = (*it).first;
}
}
}
- bool addedLemma = false;
- //do splitting on demand
- if( level==Theory::EFFORT_FULL || options::ufssEagerSplits() ){
- Debug("uf-ss-debug") << "Add splits?" << std::endl;
- //see if we have any recommended splits from large regions
- for( int i=0; i<(int)d_regions_index; i++ ){
- if( d_regions[i]->d_valid && d_regions[i]->getNumReps()>d_cardinality ){
- if( d_regions[i]->hasSplits() ){
- d_regions[i]->addSplit( out );
- addedLemma = true;
- ++( d_th->getStrongSolver()->d_statistics.d_split_lemmas );
-#ifdef ONE_SPLIT_REGION
- break;
-#endif
- }
- }
- }
+ }
+ //add lemma to output channel
+ Assert( s!=Node::null() && s.getKind()==EQUAL );
+ s = Rewriter::rewrite( s );
+ Trace("uf-ss-lemma") << "*** Split on " << s << std::endl;
+ //Trace("uf-ss-lemma") << d_th->getEqualityEngine()->areEqual( s[0], s[1] ) << " ";
+ //Trace("uf-ss-lemma") << d_th->getEqualityEngine()->areDisequal( s[0], s[1] ) << std::endl;
+ //Trace("uf-ss-lemma") << s[0].getType() << " " << s[1].getType() << std::endl;
+ //Notice() << "*** Split on " << s << std::endl;
+ //split on the equality s
+ out->split( s );
+ //tell the sat solver to explore the equals branch first
+ out->requirePhase( s, true );
+ ++( d_th->getStrongSolver()->d_statistics.d_split_lemmas );
+ return true;
+ }else{
+ return false;
+ }
+}
+
+
+void StrongSolverTheoryUf::SortRepModel::addCliqueLemma( std::vector< Node >& clique, OutputChannel* out ){
+ Assert( d_hasCard );
+ Assert( d_cardinality>0 );
+ while( clique.size()>size_t(d_cardinality+1) ){
+ clique.pop_back();
+ }
+ if( options::ufssModelInference() || Trace.isOn("uf-ss-cliques") ){
+ std::vector< Node > clique_vec;
+ clique_vec.insert( clique_vec.begin(), clique.begin(), clique.end() );
+ d_cliques[ d_cardinality ].push_back( clique_vec );
+ }
+
+ //found a clique
+ Debug("uf-ss-cliques") << "Found a clique (cardinality=" << d_cardinality << ") :" << std::endl;
+ Debug("uf-ss-cliques") << " ";
+ for( int i=0; i<(int)clique.size(); i++ ){
+ Debug("uf-ss-cliques") << clique[i] << " ";
+ }
+ Debug("uf-ss-cliques") << std::endl;
+ Debug("uf-ss-cliques") << "Finding clique disequalities..." << std::endl;
+ std::vector< Node > conflict;
+ //collect disequalities, and nodes that must be equal within representatives
+ std::map< Node, std::map< Node, bool > > explained;
+ std::map< Node, std::map< Node, bool > > nodesWithinRep;
+ for( int i=0; i<(int)d_disequalities_index; i++ ){
+ //if both sides of disequality exist in clique
+ Node r1 = d_th->d_equalityEngine.getRepresentative( d_disequalities[i][0][0] );
+ Node r2 = d_th->d_equalityEngine.getRepresentative( d_disequalities[i][0][1] );
+ if( r1!=r2 && ( explained.find( r1 )==explained.end() || explained[r1].find( r2 )==explained[r1].end() ) &&
+ std::find( clique.begin(), clique.end(), r1 )!=clique.end() &&
+ std::find( clique.begin(), clique.end(), r2 )!=clique.end() ){
+ explained[r1][r2] = true;
+ explained[r2][r1] = true;
+ conflict.push_back( d_disequalities[i] );
+ Debug("uf-ss-cliques") << " -> disequality : " << d_disequalities[i] << std::endl;
+ nodesWithinRep[r1][ d_disequalities[i][0][0] ] = true;
+ nodesWithinRep[r2][ d_disequalities[i][0][1] ] = true;
+ if( conflict.size()==(clique.size()*( clique.size()-1 )/2) ){
+ break;
}
- //force continuation via term disambiguation or combination of regions
- if( level==Theory::EFFORT_FULL ){
- if( !addedLemma ){
- Debug("uf-ss") << "No splits added." << std::endl;
- if( options::ufssColoringSat() ){
- //otherwise, try to disambiguate individual terms
- if( !disambiguateTerms( out ) ){
- //no disequalities can be propagated
- //we are in a situation where it suffices to apply a coloring to equivalence classes
- //due to our invariants, we know no coloring conflicts will occur between regions, and thus
- // we are SAT in this case.
- Debug("uf-ss-sat") << "SAT: regions = " << getNumRegions() << std::endl;
- //Notice() << "Model size for " << d_type << " is " << cardinality << ", regions = " << getNumRegions() << std::endl;
- debugPrint("uf-ss-sat");
- }
- }else{
- bool recheck = false;
- //naive strategy, force region combination involving the first valid region
- for( int i=0; i<(int)d_regions_index; i++ ){
- if( d_regions[i]->d_valid ){
- forceCombineRegion( i, false );
- recheck = true;
- break;
- }
- }
- if( recheck ){
- check( level, out );
+ }
+ }
+ //Debug("uf-ss-cliques") << conflict.size() << " " << clique.size() << std::endl;
+ Assert( (int)conflict.size()==((int)clique.size()*( (int)clique.size()-1 )/2) );
+ //Assert( (int)conflict.size()==(int)clique.size()*( (int)clique.size()-1 )/2 );
+ Debug("uf-ss-cliques") << "Finding clique equalities internal to eq classes..." << std::endl;
+ //now, we must explain equalities within each equivalence class
+ for( std::map< Node, std::map< Node, bool > >::iterator it = nodesWithinRep.begin(); it != nodesWithinRep.end(); ++it ){
+ if( it->second.size()>1 ){
+ Node prev;
+ //add explanation of t1 = t2 = ... = tn
+ Debug("uf-ss-cliques") << "Explain ";
+ for( std::map< Node, bool >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
+ if( prev!=Node::null() ){
+ Debug("uf-ss-cliques") << " = ";
+ //explain it2->first and prev
+ std::vector< TNode > expl;
+ d_th->d_equalityEngine.explainEquality( it2->first, prev, true, expl );
+ for( int i=0; i<(int)expl.size(); i++ ){
+ if( std::find( conflict.begin(), conflict.end(), expl[i] )==conflict.end() ){
+ conflict.push_back( expl[i] );
}
}
}
+ prev = it2->first;
+ Debug("uf-ss-cliques") << prev;
}
+ Debug("uf-ss-cliques") << std::endl;
}
}
+ Debug("uf-ss-cliques") << "Explanation of clique (size=" << conflict.size() << ") = " << std::endl;
+ for( int i=0; i<(int)conflict.size(); i++ ){
+ Debug("uf-ss-cliques") << conflict[i] << " ";
+ //bool value;
+ //bool hasValue = d_th->getValuation().hasSatValue( conflict[i], value );
+ //Assert( hasValue );
+ //Assert( value );
+ }
+ Debug("uf-ss-cliques") << std::endl;
+ //now, make the conflict
+#if 1
+ conflict.push_back( d_cardinality_literal[ d_cardinality ] );
+ Node conflictNode = NodeManager::currentNM()->mkNode( AND, conflict );
+ Trace("uf-ss-lemma") << "*** Add clique conflict " << conflictNode << std::endl;
+ //Notice() << "*** Add clique conflict " << conflictNode << std::endl;
+ out->conflict( conflictNode );
+ d_conflict = true;
+#else
+ Node conflictNode = conflict.size()==1 ? conflict[0] : NodeManager::currentNM()->mkNode( AND, conflict );
+ //add cardinality constraint
+ Node cardNode = d_cardinality_literal[ d_cardinality ];
+ //bool value;
+ //bool hasValue = d_th->getValuation().hasSatValue( cardNode, value );
+ //Assert( hasValue );
+ //Assert( value );
+ conflictNode = NodeManager::currentNM()->mkNode( IMPLIES, conflictNode, cardNode.notNode() );
+ Trace("uf-ss-lemma") << "*** Add clique conflict " << conflictNode << std::endl;
+ //Notice() << "*** Add clique conflict " << conflictNode << std::endl;
+ out->lemma( conflictNode );
+#endif
+ ++( d_th->getStrongSolver()->d_statistics.d_clique_lemmas );
+
+ //DO_THIS: ensure that the same clique is not reported??? Check standard effort after assertDisequal can produce same clique.
}
-void StrongSolverTheoryUf::ConflictFind::propagate( Theory::Effort level, OutputChannel* out ){
- Assert( d_cardinality>0 );
- //propagate the current cardinality as a decision literal, if not already asserted
- Node cn = d_cardinality_literal[ d_cardinality ];
- Debug("uf-ss-prop-as-dec") << "Propagate as decision " << d_type << ", cardinality = " << d_cardinality << std::endl;
- Assert( !cn.isNull() );
- if( d_cardinality_assertions.find( cn )==d_cardinality_assertions.end() ){
- //out->propagateAsDecision( d_cardinality_literal[ d_cardinality ] );
- Debug("uf-ss-prop-as-dec") << "Propagate as decision " << d_cardinality_literal[ d_cardinality ];
- Debug("uf-ss-prop-as-dec") << " " << d_cardinality_literal[ d_cardinality ][0].getType() << std::endl;
+void StrongSolverTheoryUf::SortRepModel::addTotalityAxiom( Node n, int cardinality, OutputChannel* out ){
+ Node cardLit = d_cardinality_literal[ cardinality ];
+ std::vector< Node > eqs;
+ for( int i=0; i<cardinality; i++ ){
+ eqs.push_back( n.eqNode( getTotalityLemmaTerm( cardinality, i ) ) );
}
+ Node ax = NodeManager::currentNM()->mkNode( OR, eqs );
+ Node lem = NodeManager::currentNM()->mkNode( IMPLIES, cardLit, ax );
+ Trace("uf-ss-lemma") << "*** Add totality axiom " << lem << std::endl;
+ //send as lemma to the output channel
+ d_th->getOutputChannel().lemma( lem );
+ ++( d_th->getStrongSolver()->d_statistics.d_totality_lemmas );
}
-void StrongSolverTheoryUf::ConflictFind::debugPrint( const char* c ){
+/** apply totality */
+bool StrongSolverTheoryUf::SortRepModel::applyTotality( int cardinality ){
+ return options::ufssTotality() || ( options::ufssModelInference() && !d_totality_terms[cardinality].empty() );
+}
+
+/** get totality lemma terms */
+Node StrongSolverTheoryUf::SortRepModel::getTotalityLemmaTerm( int cardinality, int i ){
+ if( options::ufssTotality() ){
+ return d_totality_terms[0][i];
+ }else{
+ return d_totality_terms[cardinality][i];
+ }
+}
+
+void StrongSolverTheoryUf::SortRepModel::debugPrint( const char* c ){
Debug( c ) << "-- Conflict Find:" << std::endl;
Debug( c ) << "Number of reps = " << d_reps << std::endl;
Debug( c ) << "Cardinality req = " << d_cardinality << std::endl;
@@ -972,7 +1161,32 @@ void StrongSolverTheoryUf::ConflictFind::debugPrint( const char* c ){
}
}
-int StrongSolverTheoryUf::ConflictFind::getNumRegions(){
+void StrongSolverTheoryUf::SortRepModel::debugModel( TheoryModel* m ){
+ std::vector< Node > eqcs;
+ eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &m->d_equalityEngine );
+ while( !eqcs_i.isFinished() ){
+ Node eqc = (*eqcs_i);
+ if( eqc.getType()==d_type ){
+ if( std::find( eqcs.begin(), eqcs.end(), eqc )==eqcs.end() ){
+ eqcs.push_back( eqc );
+ //we must ensure that this equivalence class has been accounted for
+ if( d_regions_map.find( eqc )==d_regions_map.end() ){
+ Trace("uf-ss-warn") << "WARNING : equivalence class " << eqc << " unaccounted for." << std::endl;
+ Trace("uf-ss-warn") << " type : " << d_type << std::endl;
+ Trace("uf-ss-warn") << " kind : " << eqc.getKind() << std::endl;
+ }
+ }
+ }
+ ++eqcs_i;
+ }
+ if( (int)eqcs.size()!=d_cardinality ){
+ Trace("uf-ss-warn") << "WARNING : Model does not have same # representatives as cardinality for " << d_type << "." << std::endl;
+ Trace("uf-ss-warn") << " cardinality : " << d_cardinality << std::endl;
+ Trace("uf-ss-warn") << " # reps : " << (int)eqcs.size() << std::endl;
+ }
+}
+
+int StrongSolverTheoryUf::SortRepModel::getNumRegions(){
int count = 0;
for( int i=0; i<(int)d_regions_index; i++ ){
if( d_regions[i]->d_valid ){
@@ -982,25 +1196,7 @@ int StrongSolverTheoryUf::ConflictFind::getNumRegions(){
return count;
}
-void StrongSolverTheoryUf::ConflictFind::setCardinality( int c, OutputChannel* out ){
- d_cardinality = c;
- //add appropriate lemma
- Node lem = getCardinalityLemma();
- out->lemma( lem );
- //add the appropriate lemma
- Debug("uf-ss-fmf") << "Set cardinality " << d_type << " = " << c << std::endl;
- Debug("uf-ss-prop-as-dec") << "Propagate as decision " << lem[0] << std::endl;
- //out->propagateAsDecision( lem[0] );
- d_is_cardinality_requested = true;
- d_is_cardinality_requested_c = true;
- //now, require old literal to be decided false
- //if( d_cardinality_literal.find( c-1 )!=d_cardinality_literal.end() ){
- // Debug("uf-ss-req-phase") << "Require phase " << d_cardinality_literal[c-1] << " = false " << std::endl;
- // out->requirePhase( d_cardinality_literal[c-1], false );
- //}
-}
-
-void StrongSolverTheoryUf::ConflictFind::getRepresentatives( std::vector< Node >& reps ){
+void StrongSolverTheoryUf::SortRepModel::getRepresentatives( std::vector< Node >& reps ){
if( !options::ufssColoringSat() ){
bool foundRegion = false;
for( int i=0; i<(int)d_regions_index; i++ ){
@@ -1019,87 +1215,158 @@ void StrongSolverTheoryUf::ConflictFind::getRepresentatives( std::vector< Node >
}
}
-bool StrongSolverTheoryUf::ConflictFind::minimize( OutputChannel* out ){
- //ensure that model forms a clique:
- // if two equivalence classes are neither equal nor disequal, add a split
- int validRegionIndex = -1;
- for( int i=0; i<(int)d_regions_index; i++ ){
- if( d_regions[i]->d_valid ){
- if( validRegionIndex!=-1 ){
- combineRegions( validRegionIndex, i );
- if( !d_regions[validRegionIndex]->minimize( out ) ){
- return false;
+
+/** initialize */
+void StrongSolverTheoryUf::InfRepModel::initialize( OutputChannel* out ){
+
+}
+
+/** new node */
+void StrongSolverTheoryUf::InfRepModel::newEqClass( Node n ){
+ d_rep[n] = n;
+ //d_const_rep[n] = n.getMetaKind()==metakind::CONSTANT;
+}
+
+/** merge */
+void StrongSolverTheoryUf::InfRepModel::merge( Node a, Node b ){
+ //d_rep[b] = false;
+ //d_const_rep[a] = d_const_rep[a] || d_const_rep[b];
+ Node repb = d_rep[b];
+ Assert( !repb.isNull() );
+ if( repb.getMetaKind()==metakind::CONSTANT || isBadRepresentative( d_rep[a] ) ){
+ d_rep[a] = repb;
+ }
+ d_rep[b] = Node::null();
+}
+
+/** check */
+void StrongSolverTheoryUf::InfRepModel::check( Theory::Effort level, OutputChannel* out ){
+
+}
+
+/** minimize */
+bool StrongSolverTheoryUf::InfRepModel::minimize( OutputChannel* out ){
+#if 0
+ bool retVal = true;
+#else
+ bool retVal = !addSplit( out );
+#endif
+ if( retVal ){
+ std::vector< Node > reps;
+ getRepresentatives( reps );
+ Trace("uf-ss-fmf") << "Num representatives of type " << d_type << " : " << reps.size() << std::endl;
+ /*
+ for( int i=0; i<(int)reps.size(); i++ ){
+ std::cout << reps[i] << " ";
+ }
+ std::cout << std::endl;
+ for( int i=0; i<(int)reps.size(); i++ ){
+ std::cout << reps[i].getMetaKind() << " ";
+ }
+ std::cout << std::endl;
+ for( NodeNodeMap::iterator it = d_rep.begin(); it != d_rep.end(); ++it ){
+ Node rep = (*it).second;
+ if( !rep.isNull() && !isBadRepresentative( rep ) ){
+ for( NodeNodeMap::iterator it2 = d_rep.begin(); it2 != d_rep.end(); ++it2 ){
+ Node rep2 = (*it2).second;
+ if( !rep2.isNull() && !isBadRepresentative( rep2 ) ){
+ if( d_th->getQuantifiersEngine()->getEqualityQuery()->areDisequal( rep, rep2 ) ){
+ std::cout << "1 ";
+ }else{
+ std::cout << "0 ";
+ }
+ }
}
- }else{
- validRegionIndex = i;
+ //std::cout << " : " << rep;
+ std::cout << std::endl;
}
}
+ */
}
- if( !d_regions[validRegionIndex]->minimize( out ) ){
- return false;
+ return retVal;
+}
+
+/** get representatives */
+void StrongSolverTheoryUf::InfRepModel::getRepresentatives( std::vector< Node >& reps ){
+ for( NodeNodeMap::iterator it = d_rep.begin(); it != d_rep.end(); ++it ){
+ if( !(*it).second.isNull() ){
+ reps.push_back( (*it).first );
+ }
}
- return true;
}
-Node StrongSolverTheoryUf::ConflictFind::getCardinalityLemma(){
- if( d_cardinality_lemma.find( d_cardinality )==d_cardinality_lemma.end() ){
- if( d_cardinality_lemma_term.isNull() ){
- std::stringstream ss;
- ss << Expr::setlanguage(options::outputLanguage());
- ss << "t_" << d_type;
- d_cardinality_lemma_term = NodeManager::currentNM()->mkSkolem( ss.str(), d_type );
+/** add split function */
+bool StrongSolverTheoryUf::InfRepModel::addSplit( OutputChannel* out ){
+ std::vector< Node > visited;
+ for( NodeNodeMap::iterator it = d_rep.begin(); it != d_rep.end(); ++it ){
+ Node rep = (*it).second;
+ if( !rep.isNull() && !isBadRepresentative( rep ) ){
+ bool constRep = rep.getMetaKind()==metakind::CONSTANT;
+ for( size_t i=0; i<visited.size(); i++ ){
+ if( !constRep || !visited[i].getMetaKind()==metakind::CONSTANT ){
+ if( !d_th->getQuantifiersEngine()->getEqualityQuery()->areDisequal( rep, visited[i] ) ){
+ //split on these nodes
+ Node eq = rep.eqNode( visited[i] );
+ Trace("uf-ss-lemma") << "*** Split on " << eq << std::endl;
+ eq = Rewriter::rewrite( eq );
+ Debug("uf-ss-lemma-debug") << "Rewritten " << eq << std::endl;
+ out->split( eq );
+ //explore the equals branch first
+ out->requirePhase( eq, true );
+ ++( d_th->getStrongSolver()->d_statistics.d_split_lemmas );
+ return true;
+ }
+ }
+ }
+ visited.push_back( rep );
}
- Node lem = NodeManager::currentNM()->mkNode( CARDINALITY_CONSTRAINT, d_cardinality_lemma_term,
- NodeManager::currentNM()->mkConst( Rational( d_cardinality ) ) );
- lem = Rewriter::rewrite(lem);
- d_cardinality_literal[ d_cardinality ] = lem;
- lem = NodeManager::currentNM()->mkNode( OR, lem, lem.notNode() );
- d_cardinality_lemma[ d_cardinality ] = lem;
}
- return d_cardinality_lemma[ d_cardinality ];
+ return false;
+}
+
+bool StrongSolverTheoryUf::InfRepModel::isBadRepresentative( Node n ){
+ return n.getKind()==kind::PLUS;
}
StrongSolverTheoryUf::StrongSolverTheoryUf(context::Context* c, context::UserContext* u, OutputChannel& out, TheoryUF* th) :
d_out( &out ),
d_th( th ),
-d_conf_find(),
+d_conflict( c, false ),
+d_rep_model(),
d_conf_types(),
-d_conf_find_init( c )
+d_rep_model_init( c )
{
-
+ if( options::ufssColoringSat() ){
+ d_term_amb = new TermDisambiguator( th->getQuantifiersEngine(), c );
+ }else{
+ d_term_amb = NULL;
+ }
}
/** new node */
void StrongSolverTheoryUf::newEqClass( Node n ){
- TypeNode tn = n.getType();
- ConflictFind* c = getConflictFind( tn );
+ RepModel* c = getRepModel( n );
if( c ){
- Debug("uf-ss-solver") << "StrongSolverTheoryUf: New eq class " << n << " " << tn << std::endl;
+ Trace("uf-ss-solver") << "StrongSolverTheoryUf: New eq class " << n << " : " << n.getType() << std::endl;
c->newEqClass( n );
}
- //else if( tn.isSort() ){
- // //Debug("uf-ss-solver") << "WAIT: StrongSolverTheoryUf: New eq class " << n << " " << tn << std::endl;
- // //d_new_eq_class_waiting[tn].push_back( n );
- //}
}
/** merge */
void StrongSolverTheoryUf::merge( Node a, Node b ){
- TypeNode tn = a.getType();
- ConflictFind* c = getConflictFind( tn );
+ RepModel* c = getRepModel( a );
if( c ){
- Debug("uf-ss-solver") << "StrongSolverTheoryUf: Merge " << a << " " << b << " " << tn << std::endl;
+ Trace("uf-ss-solver") << "StrongSolverTheoryUf: Merge " << a << " " << b << " : " << a.getType() << std::endl;
c->merge( a, b );
}
}
/** assert terms are disequal */
void StrongSolverTheoryUf::assertDisequal( Node a, Node b, Node reason ){
- TypeNode tn = a.getType();
- ConflictFind* c = getConflictFind( tn );
+ RepModel* c = getRepModel( a );
if( c ){
- Debug("uf-ss-solver") << "StrongSolverTheoryUf: Assert disequal " << a << " " << b << " " << tn << std::endl;
+ Trace("uf-ss-solver") << "StrongSolverTheoryUf: Assert disequal " << a << " " << b << " : " << a.getType() << std::endl;
//Assert( d_th->d_equalityEngine.getRepresentative( a )==a );
//Assert( d_th->d_equalityEngine.getRepresentative( b )==b );
c->assertDisequal( a, b, reason );
@@ -1108,88 +1375,89 @@ void StrongSolverTheoryUf::assertDisequal( Node a, Node b, Node reason ){
/** assert a node */
void StrongSolverTheoryUf::assertNode( Node n, bool isDecision ){
- Debug("uf-ss-assert") << "Assert " << n << " " << isDecision << std::endl;
+ Trace("uf-ss") << "Assert " << n << " " << isDecision << std::endl;
if( n.getKind()==CARDINALITY_CONSTRAINT ){
TypeNode tn = n[0].getType();
- Assert( d_conf_find[tn]->getCardinality()>0 );
Assert( tn.isSort() );
- Assert( d_conf_find[tn] );
+ Assert( d_rep_model[tn] );
long nCard = n[1].getConst<Rational>().getNumerator().getLong();
- d_conf_find[tn]->assertCardinality( nCard, true );
- if( nCard==d_conf_find[tn]->getCardinality() ){
- d_conf_find[tn]->d_is_cardinality_set = true;
- d_conf_find[tn]->d_is_cardinality_requested = false;
- d_conf_find[tn]->d_is_cardinality_requested_c = false;
- }
+ d_rep_model[tn]->assertCardinality( d_out, nCard, true );
}else if( n.getKind()==NOT && n[0].getKind()==CARDINALITY_CONSTRAINT ){
- //must add new lemma
Node nn = n[0];
TypeNode tn = nn[0].getType();
Assert( tn.isSort() );
- Assert( d_conf_find[tn] );
+ Assert( d_rep_model[tn] );
long nCard = nn[1].getConst<Rational>().getNumerator().getLong();
- d_conf_find[tn]->assertCardinality( nCard, false );
- if( nCard==d_conf_find[tn]->getCardinality() ){
- AlwaysAssert(!isDecision, "Error: Negative cardinality node decided upon");
- Debug("uf-ss-fmf") << "No model of size " << d_conf_find[tn]->getCardinality() << " exists for type " << tn << std::endl;
- //Notice() << "No model of size " << d_conf_find[tn]->getCardinality() << " exists for type " << tn << std::endl;
- //increment to next cardinality
- d_statistics.d_max_model_size.maxAssign( d_conf_find[tn]->getCardinality() + 1 );
- d_conf_find[tn]->setCardinality( d_conf_find[tn]->getCardinality() + 1, d_out );
- //Notice() << d_conf_find[tn]->getCardinality() << " ";
- ////give up permanently on this cardinality
- //d_out->lemma( n );
- }
+ d_rep_model[tn]->assertCardinality( d_out, nCard, false );
}else{
////FIXME: this is too strict: theory propagations are showing up as isDecision=true, but
//// a theory propagation is not a decision.
- //if( isDecision ){
- // for( std::map< TypeNode, ConflictFind* >::iterator it = d_conf_find.begin(); it != d_conf_find.end(); ++it ){
- // if( !it->second->hasCardinalityAsserted() ){
- // Notice() << "Assert " << n << " " << isDecision << std::endl;
- // Notice() << "Error: constraint asserted before cardinality for " << it->first << std::endl;
- // Unimplemented();
- // }
- // }
- //}
+ if( isDecision ){
+ for( std::map< TypeNode, RepModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
+ if( !it->second->hasCardinalityAsserted() ){
+ Trace("uf-ss-warn") << "WARNING: Assert " << n << " as a decision before cardinality for " << it->first << "." << std::endl;
+ //Message() << "Error: constraint asserted before cardinality for " << it->first << std::endl;
+ //Unimplemented();
+ }
+ }
+ }
}
+ Trace("uf-ss") << "Assert: done " << n << " " << isDecision << std::endl;
}
/** check */
void StrongSolverTheoryUf::check( Theory::Effort level ){
- Debug("uf-ss-solver") << "StrongSolverTheoryUf: check " << level << std::endl;
- if( level==Theory::EFFORT_FULL ){
- debugPrint( "uf-ss-debug" );
- }
- for( std::map< TypeNode, ConflictFind* >::iterator it = d_conf_find.begin(); it != d_conf_find.end(); ++it ){
- it->second->check( level, d_out );
+ if( !d_conflict ){
+ Trace("uf-ss-solver") << "StrongSolverTheoryUf: check " << level << std::endl;
+ if( level==Theory::EFFORT_FULL ){
+ debugPrint( "uf-ss-debug" );
+ }
+ for( std::map< TypeNode, RepModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
+ it->second->check( level, d_out );
+ if( it->second->isConflict() ){
+ d_conflict = true;
+ break;
+ }
+ }
+ //disambiguate terms if necessary
+ if( !d_conflict && level==Theory::EFFORT_FULL && options::ufssColoringSat() ){
+ Assert( d_term_amb!=NULL );
+ d_statistics.d_disamb_term_lemmas += d_term_amb->disambiguateTerms( d_out );
+ }
+ Trace("uf-ss-solver") << "Done StrongSolverTheoryUf: check " << level << std::endl;
}
- Debug("uf-ss-solver") << "Done StrongSolverTheoryUf: check " << level << std::endl;
}
/** propagate */
void StrongSolverTheoryUf::propagate( Theory::Effort level ){
- for( std::map< TypeNode, ConflictFind* >::iterator it = d_conf_find.begin(); it != d_conf_find.end(); ++it ){
- it->second->propagate( level, d_out );
- }
+ //for( std::map< TypeNode, RepModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
+ // it->second->propagate( level, d_out );
+ //}
}
-void StrongSolverTheoryUf::preRegisterTerm( TNode n ){
- //shouldn't have to preregister this type (it may be that there are no quantifiers over tn) FIXME
- TypeNode tn = n.getType();
- if( tn.isSort() ){
- preRegisterType( tn );
+/** get next decision request */
+Node StrongSolverTheoryUf::getNextDecisionRequest(){
+ for( std::map< TypeNode, RepModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
+ Node n = it->second->getNextDecisionRequest();
+ if( !n.isNull() ){
+ return n;
+ }
}
+ return Node::null();
}
-void StrongSolverTheoryUf::registerQuantifier( Node f ){
- Debug("uf-ss-register") << "Register quantifier " << f << std::endl;
- //must ensure the quantifier does not quantify over arithmetic
- for( int i=0; i<(int)f[0].getNumChildren(); i++ ){
- TypeNode tn = f[0][i].getType();
+void StrongSolverTheoryUf::preRegisterTerm( TNode n ){
+ //shouldn't have to preregister this type (it may be that there are no quantifiers over tn)
+ TypeNode tn = n.getType();
+ if( d_rep_model.find( tn )==d_rep_model.end() ){
+ RepModel* rm = NULL;
if( tn.isSort() ){
- preRegisterType( tn );
+ Debug("uf-ss-register") << "Preregister sort " << tn << "." << std::endl;
+ rm = new SortRepModel( n, d_th->getSatContext(), d_th );
+ }else if( tn.isInteger() ){
+ //rm = new InfRepModel( tn, d_th->getSatContext(), d_th );
+ //rm = new SortRepModel( tn, d_th->getSatContext(), d_th );
}else{
/*
if( tn==NodeManager::currentNM()->integerType() || tn==NodeManager::currentNM()->realType() ){
@@ -1205,63 +1473,51 @@ void StrongSolverTheoryUf::registerQuantifier( Node f ){
}
*/
}
+ if( rm ){
+ rm->initialize( d_out );
+ d_rep_model[tn] = rm;
+ d_rep_model_init[tn] = true;
+ }
}
}
-void StrongSolverTheoryUf::preRegisterType( TypeNode tn ){
- if( d_conf_find.find( tn )==d_conf_find.end() ){
- Debug("uf-ss-register") << "Preregister " << tn << "." << std::endl;
- //enter into incremental finite model finding mode: try cardinality = 1 first
- //if( !d_conf_types.empty() ){
- // Debug("uf-ss-na") << "Strong solver unimplemented for multiple sorts." << std::endl;
- // Unimplemented();
- //}
- d_conf_find[tn] = new ConflictFind( tn, d_th->getSatContext(), d_th );
- //assign cardinality restriction
- d_statistics.d_max_model_size.maxAssign( 1 );
- d_conf_find[tn]->setCardinality( 1, d_out );
- ////add waiting equivalence classes now
- //if( !d_new_eq_class_waiting[tn].empty() ){
- // Debug("uf-ss-register") << "Add " << (int)d_new_eq_class_waiting[tn].size() << " new eq classes." << std::endl;
- // for( int i=0; i<(int)d_new_eq_class_waiting[tn].size(); i++ ){
- // newEqClass( d_new_eq_class_waiting[tn][i] );
- // }
- // d_new_eq_class_waiting[tn].clear();
- //}
- d_conf_types.push_back( tn );
- }
+void StrongSolverTheoryUf::registerQuantifier( Node f ){
+ Debug("uf-ss-register") << "Register quantifier " << f << std::endl;
+ //must ensure the quantifier does not quantify over arithmetic
+ //for( int i=0; i<(int)f[0].getNumChildren(); i++ ){
+ // TypeNode tn = f[0][i].getType();
+ // preRegisterType( tn, true );
+ //}
}
-StrongSolverTheoryUf::ConflictFind* StrongSolverTheoryUf::getConflictFind( TypeNode tn ){
- std::map< TypeNode, ConflictFind* >::iterator it = d_conf_find.find( tn );
+
+StrongSolverTheoryUf::RepModel* StrongSolverTheoryUf::getRepModel( Node n ){
+ TypeNode tn = n.getType();
+ std::map< TypeNode, RepModel* >::iterator it = d_rep_model.find( tn );
//pre-register the type if not done already
- if( it==d_conf_find.end() ){
- if( tn.isSort() ){
- preRegisterType( tn );
- it = d_conf_find.find( tn );
- }
+ if( it==d_rep_model.end() ){
+ preRegisterTerm( n );
+ it = d_rep_model.find( tn );
}
- if( it!=d_conf_find.end() ){
+ if( it!=d_rep_model.end() ){
//initialize the type if necessary
- if( d_conf_find_init.find( tn )==d_conf_find_init.end() ){
- //assign cardinality restriction
- d_statistics.d_max_model_size.maxAssign( 1 );
- it->second->setCardinality( 1, d_out );
- d_conf_find_init[tn] = true;
- }
+ //if( d_rep_model_init.find( tn )==d_rep_model_init.end() ){
+ ////initialize the model
+ //it->second->initialize( d_out );
+ //d_rep_model_init[tn] = true;
+ //}
return it->second;
- }else{
- return NULL;
}
+ return NULL;
}
void StrongSolverTheoryUf::notifyRestart(){
- Debug("uf-ss-prop-as-dec") << "Restart?" << std::endl;
+
}
/** get cardinality for sort */
-int StrongSolverTheoryUf::getCardinality( TypeNode t ) {
- ConflictFind* c = getConflictFind( t );
+int StrongSolverTheoryUf::getCardinality( Node n ) {
+ RepModel* c = getRepModel( n );
if( c ){
return c->getCardinality();
}else{
@@ -1269,28 +1525,22 @@ int StrongSolverTheoryUf::getCardinality( TypeNode t ) {
}
}
-void StrongSolverTheoryUf::getRepresentatives( TypeNode t, std::vector< Node >& reps ){
- ConflictFind* c = getConflictFind( t );
+void StrongSolverTheoryUf::getRepresentatives( Node n, std::vector< Node >& reps ){
+ RepModel* c = getRepModel( n );
if( c ){
c->getRepresentatives( reps );
}
}
-//Node StrongSolverTheoryUf::getCardinalityTerm( TypeNode t ){
-// ConflictFind* c = getConflictFind( t );
-// if( c ){
-// return c->getCardinalityTerm();
-// }else{
-// return Node::null();
-// }
-//}
-
-bool StrongSolverTheoryUf::minimize(){
- for( std::map< TypeNode, ConflictFind* >::iterator it = d_conf_find.begin(); it != d_conf_find.end(); ++it ){
- if( !it->second->minimize( d_out ) ){
+bool StrongSolverTheoryUf::minimize( TheoryModel* m ){
+ for( std::map< TypeNode, RepModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
+ if( !it->second->minimize( d_out, m ) ){
return false;
}
}
+ for( std::map< TypeNode, RepModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
+ Trace("uf-ss-minimize") << "Cardinality( " << it->first << " ) : " << it->second->getCardinality() << std::endl;
+ }
return true;
}
@@ -1309,22 +1559,32 @@ void StrongSolverTheoryUf::debugPrint( const char* c ){
// eqc_iter++;
//}
- for( std::map< TypeNode, ConflictFind* >::iterator it = d_conf_find.begin(); it != d_conf_find.end(); ++it ){
+ for( std::map< TypeNode, RepModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
Debug( c ) << "Conflict find structure for " << it->first << ": " << std::endl;
it->second->debugPrint( c );
Debug( c ) << std::endl;
}
}
+void StrongSolverTheoryUf::debugModel( TheoryModel* m ){
+ if( Trace.isOn("uf-ss-warn") ){
+ for( std::map< TypeNode, RepModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
+ it->second->debugModel( m );
+ }
+ }
+}
+
StrongSolverTheoryUf::Statistics::Statistics():
d_clique_lemmas("StrongSolverTheoryUf::Clique_Lemmas", 0),
d_split_lemmas("StrongSolverTheoryUf::Split_Lemmas", 0),
d_disamb_term_lemmas("StrongSolverTheoryUf::Disambiguate_Term_Lemmas", 0),
- d_max_model_size("StrongSolverTheoryUf::Max_Model_Size", 0)
+ d_totality_lemmas("StrongSolverTheoryUf::Totality_Lemmas", 0),
+ d_max_model_size("StrongSolverTheoryUf::Max_Model_Size", 1)
{
StatisticsRegistry::registerStat(&d_clique_lemmas);
StatisticsRegistry::registerStat(&d_split_lemmas);
StatisticsRegistry::registerStat(&d_disamb_term_lemmas);
+ StatisticsRegistry::registerStat(&d_totality_lemmas);
StatisticsRegistry::registerStat(&d_max_model_size);
}
@@ -1332,10 +1592,70 @@ StrongSolverTheoryUf::Statistics::~Statistics(){
StatisticsRegistry::unregisterStat(&d_clique_lemmas);
StatisticsRegistry::unregisterStat(&d_split_lemmas);
StatisticsRegistry::unregisterStat(&d_disamb_term_lemmas);
+ StatisticsRegistry::unregisterStat(&d_totality_lemmas);
StatisticsRegistry::unregisterStat(&d_max_model_size);
}
-bool StrongSolverTheoryUf::involvesRelevantType( Node n ){
+
+int TermDisambiguator::disambiguateTerms( OutputChannel* out ){
+ Debug("uf-ss-disamb") << "Disambiguate terms." << std::endl;
+ int lemmaAdded = 0;
+ //otherwise, determine ambiguous pairs of ground terms for relevant sorts
+ quantifiers::TermDb* db = d_qe->getTermDatabase();
+ for( std::map< Node, std::vector< Node > >::iterator it = db->d_op_map.begin(); it != db->d_op_map.end(); ++it ){
+ Debug("uf-ss-disamb") << "Check " << it->first << std::endl;
+ if( it->second.size()>1 ){
+ if(involvesRelevantType( it->second[0] ) ){
+ for( int i=0; i<(int)it->second.size(); i++ ){
+ for( int j=(i+1); j<(int)it->second.size(); j++ ){
+ Kind knd = it->second[i].getType()==NodeManager::currentNM()->booleanType() ? IFF : EQUAL;
+ Node eq = NodeManager::currentNM()->mkNode( knd, it->second[i], it->second[j] );
+ eq = Rewriter::rewrite(eq);
+ //determine if they are ambiguous
+ if( d_term_amb.find( eq )==d_term_amb.end() ){
+ Debug("uf-ss-disamb") << "Check disambiguate " << it->second[i] << " " << it->second[j] << std::endl;
+ d_term_amb[ eq ] = true;
+ //if they are equal
+ if( d_qe->getEqualityQuery()->areEqual( it->second[i], it->second[j] ) ){
+ d_term_amb[ eq ] = false;
+ }else{
+ //if an argument is disequal, then they are not ambiguous
+ for( int k=0; k<(int)it->second[i].getNumChildren(); k++ ){
+ if( d_qe->getEqualityQuery()->areDisequal( it->second[i][k], it->second[j][k] ) ){
+ d_term_amb[ eq ] = false;
+ break;
+ }
+ }
+ }
+ if( d_term_amb[ eq ] ){
+ Debug("uf-ss-disamb") << "Disambiguate " << it->second[i] << " " << it->second[j] << std::endl;
+ //must add lemma
+ std::vector< Node > children;
+ children.push_back( eq );
+ for( int k=0; k<(int)it->second[i].getNumChildren(); k++ ){
+ Kind knd2 = it->second[i][k].getType()==NodeManager::currentNM()->booleanType() ? IFF : EQUAL;
+ Node eqc = NodeManager::currentNM()->mkNode( knd2, it->second[i][k], it->second[j][k] );
+ children.push_back( eqc.notNode() );
+ }
+ Assert( children.size()>1 );
+ Node lem = NodeManager::currentNM()->mkNode( OR, children );
+ Debug( "uf-ss-lemma" ) << "*** Disambiguate lemma : " << lem << std::endl;
+ //Notice() << "*** Disambiguate lemma : " << lem << std::endl;
+ out->lemma( lem );
+ d_term_amb[ eq ] = false;
+ lemmaAdded++;
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+ Debug("uf-ss-disamb") << "Done disambiguate terms. " << lemmaAdded << std::endl;
+ return lemmaAdded;
+}
+
+bool TermDisambiguator::involvesRelevantType( Node n ){
if( n.getKind()==APPLY_UF ){
for( int i=0; i<(int)n.getNumChildren(); i++ ){
if( n[i].getType().isSort() ){
diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h
index 479fea05f..8c63b4308 100644
--- a/src/theory/uf/theory_uf_strong_solver.h
+++ b/src/theory/uf/theory_uf_strong_solver.h
@@ -32,24 +32,63 @@ namespace theory {
namespace uf {
class TheoryUF;
+class TermDisambiguator;
class StrongSolverTheoryUf{
protected:
typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
+ typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
typedef context::CDChunkList<Node> NodeList;
typedef context::CDList<bool> BoolList;
typedef context::CDList<bool> IntList;
typedef context::CDHashMap<TypeNode, bool, TypeNodeHashFunction> TypeNodeBoolMap;
public:
+ class RepModel {
+ protected:
+ /** type */
+ TypeNode d_type;
+ public:
+ RepModel( TypeNode tn ) : d_type( tn ){}
+ virtual ~RepModel(){}
+ /** initialize */
+ virtual void initialize( OutputChannel* out ) = 0;
+ /** new node */
+ virtual void newEqClass( Node n ) = 0;
+ /** merge */
+ virtual void merge( Node a, Node b ) = 0;
+ /** assert terms are disequal */
+ virtual void assertDisequal( Node a, Node b, Node reason ) = 0;
+ /** check */
+ virtual void check( Theory::Effort level, OutputChannel* out ){}
+ /** get next decision request */
+ virtual Node getNextDecisionRequest() { return Node::null(); }
+ /** minimize */
+ virtual bool minimize( OutputChannel* out, TheoryModel* m ){ return true; }
+ /** assert cardinality */
+ virtual void assertCardinality( OutputChannel* out, int c, bool val ){}
+ /** is in conflict */
+ virtual bool isConflict() { return false; }
+ /** get cardinality */
+ virtual int getCardinality() { return -1; }
+ /** has cardinality */
+ virtual bool hasCardinalityAsserted() { return true; }
+ /** get representatives */
+ virtual void getRepresentatives( std::vector< Node >& reps ){}
+ /** print debug */
+ virtual void debugPrint( const char* c ){}
+ /** debug a model */
+ virtual void debugModel( TheoryModel* m ){}
+ };
+public:
/** information for incremental conflict/clique finding for a particular sort */
- class ConflictFind {
+ class SortRepModel : public RepModel {
public:
/** a partition of the current equality graph for which cliques can occur internally */
class Region {
public:
/** conflict find pointer */
- ConflictFind* d_cf;
+ SortRepModel* d_cf;
/** information stored about each node in region */
class RegionNodeInfo {
public:
@@ -86,14 +125,13 @@ public:
};
///** end class RegionNodeInfo */
private:
+ context::CDO< unsigned > d_testCliqueSize;
+ context::CDO< unsigned > d_splitsSize;
+ public:
//a postulated clique
NodeBoolMap d_testClique;
- context::CDO< unsigned > d_testCliqueSize;
//disequalities needed for this clique to happen
NodeBoolMap d_splits;
- context::CDO< unsigned > d_splitsSize;
- /** get split */
- Node getBestSplit();
private:
//number of valid representatives in this region
context::CDO< unsigned > d_reps_size;
@@ -106,11 +144,11 @@ public:
void setRep( Node n, bool valid );
public:
//constructor
- Region( ConflictFind* cf, context::Context* c ) : d_cf( cf ), d_testClique( c ), d_testCliqueSize( c, 0 ),
- d_splits( c ), d_splitsSize( c, 0 ), d_reps_size( c, 0 ), d_total_diseq_external( c, 0 ),
- d_total_diseq_internal( c, 0 ), d_valid( c, true ) {
+ Region( SortRepModel* cf, context::Context* c ) : d_cf( cf ), d_testCliqueSize( c, 0 ),
+ d_splitsSize( c, 0 ), d_testClique( c ), d_splits( c ), d_reps_size( c, 0 ),
+ d_total_diseq_external( c, 0 ), d_total_diseq_internal( c, 0 ), d_valid( c, true ) {
}
- ~Region(){}
+ virtual ~Region(){}
//region node infomation
std::map< Node, RegionNodeInfo* > d_nodes;
//whether region is valid
@@ -146,10 +184,6 @@ public:
public:
/** check for cliques */
bool check( Theory::Effort level, int cardinality, std::vector< Node >& clique );
- /** add split */
- void addSplit( OutputChannel* out );
- /** minimize */
- bool minimize( OutputChannel* out );
//print debug
void debugPrint( const char* c, bool incClique = false );
};
@@ -162,25 +196,23 @@ public:
std::vector< Region* > d_regions;
/** map from Nodes to index of d_regions they exist in, -1 means invalid */
NodeIntMap d_regions_map;
+ /** the score for each node for splitting */
+ NodeIntMap d_split_score;
/** regions used to d_region_index */
context::CDO< unsigned > d_disequalities_index;
/** list of all disequalities */
std::vector< Node > d_disequalities;
/** number of representatives in all regions */
context::CDO< unsigned > d_reps;
- /** whether two terms are ambiguous (indexed by equalities) */
- NodeBoolMap d_term_amb;
private:
/** get number of disequalities from node n to region ri */
int getNumDisequalitiesToRegion( Node n, int ri );
/** get number of disequalities from Region r to other regions */
void getDisequalitiesToRegions( int ri, std::map< int, int >& regions_diseq );
- /** explain clique */
- void explainClique( std::vector< Node >& clique, OutputChannel* out );
/** is valid */
bool isValid( int ri ) { return ri>=0 && ri<(int)d_regions_index && d_regions[ ri ]->d_valid; }
- /** check ambiguous terms */
- bool disambiguateTerms( OutputChannel* out );
+ /** set split score */
+ void setSplitScore( Node n, int s );
private:
/** check if we need to combine region ri */
void checkRegion( int ri, bool rec = true );
@@ -191,78 +223,131 @@ public:
/** move node n to region ri */
void moveNode( Node n, int ri );
private:
- /** cardinality operating with */
+ /** allocate cardinality */
+ void allocateCardinality( OutputChannel* out );
+ /** add split */
+ bool addSplit( Region* r, OutputChannel* out );
+ /** add clique lemma */
+ void addCliqueLemma( std::vector< Node >& clique, OutputChannel* out );
+ /** add totality axiom */
+ void addTotalityAxiom( Node n, int cardinality, OutputChannel* out );
+ private:
+ /** Are we in conflict */
+ context::CDO<bool> d_conflict;
+ /** cardinality */
context::CDO< int > d_cardinality;
- /** type */
- TypeNode d_type;
+ /** maximum allocated cardinality */
+ int d_aloc_cardinality;
/** cardinality lemma term */
- Node d_cardinality_lemma_term;
+ Node d_cardinality_term;
+ /** cardinality totality terms */
+ std::map< int, std::vector< Node > > d_totality_terms;
/** cardinality literals */
std::map< int, Node > d_cardinality_literal;
/** cardinality lemmas */
std::map< int, Node > d_cardinality_lemma;
/** cardinality assertions (indexed by cardinality literals ) */
NodeBoolMap d_cardinality_assertions;
+ /** whether a positive cardinality constraint has been asserted */
+ context::CDO< bool > d_hasCard;
+ /** clique lemmas that have been asserted */
+ std::map< int, std::vector< std::vector< Node > > > d_cliques;
+ private:
+ /** apply totality */
+ bool applyTotality( int cardinality );
+ /** get totality lemma terms */
+ Node getTotalityLemmaTerm( int cardinality, int i );
public:
- ConflictFind( TypeNode tn, context::Context* c, TheoryUF* th ) :
- d_th( th ), d_regions_index( c, 0 ), d_regions_map( c ), d_disequalities_index( c, 0 ),
- d_reps( c, 0 ), d_term_amb( c ), d_cardinality( c, 1 ), d_type( tn ),
- d_cardinality_assertions( c ), d_is_cardinality_set( c, false ),
- d_is_cardinality_requested_c( c, false ), d_is_cardinality_requested( false ), d_hasCard( c, false ){}
- ~ConflictFind(){}
+ SortRepModel( Node n, context::Context* c, TheoryUF* th );
+ virtual ~SortRepModel(){}
+ /** initialize */
+ void initialize( OutputChannel* out );
/** new node */
void newEqClass( Node n );
/** merge */
void merge( Node a, Node b );
/** assert terms are disequal */
void assertDisequal( Node a, Node b, Node reason );
- /** assert cardinality */
- void assertCardinality( int c, bool val );
- /** whether cardinality has been asserted */
- bool hasCardinalityAsserted() { return d_hasCard; }
/** check */
void check( Theory::Effort level, OutputChannel* out );
/** propagate */
void propagate( Theory::Effort level, OutputChannel* out );
- //print debug
- void debugPrint( const char* c );
- /** set cardinality */
- void setCardinality( int c, OutputChannel* out );
+ /** get next decision request */
+ Node getNextDecisionRequest();
+ /** minimize */
+ bool minimize( OutputChannel* out, TheoryModel* m );
+ /** assert cardinality */
+ void assertCardinality( OutputChannel* out, int c, bool val );
+ /** is in conflict */
+ bool isConflict() { return d_conflict; }
/** get cardinality */
int getCardinality() { return d_cardinality; }
/** get representatives */
void getRepresentatives( std::vector< Node >& reps );
- /** get model basis term */
- //Node getCardinalityTerm() { return d_cardinality_lemma_term; }
- /** minimize */
- bool minimize( OutputChannel* out );
- /** get cardinality lemma */
- Node getCardinalityLemma();
+ /** has cardinality */
+ bool hasCardinalityAsserted() { return d_hasCard; }
+ //print debug
+ void debugPrint( const char* c );
+ /** debug a model */
+ void debugModel( TheoryModel* m );
public:
/** get number of regions (for debugging) */
int getNumRegions();
- /** is cardinality set */
- context::CDO< bool > d_is_cardinality_set;
- context::CDO< bool > d_is_cardinality_requested_c;
- bool d_is_cardinality_requested;
- /** whether a positive cardinality constraint has been asserted */
- context::CDO< bool > d_hasCard;
- }; /** class ConflictFind */
+ }; /** class SortRepModel */
+private:
+ /** infinite rep model */
+ class InfRepModel : public RepModel
+ {
+ protected:
+ /** theory uf pointer */
+ TheoryUF* d_th;
+ /** list of representatives */
+ NodeNodeMap d_rep;
+ /** whether representatives are constant */
+ NodeBoolMap d_const_rep;
+ /** add split */
+ bool addSplit( OutputChannel* out );
+ /** is bad representative */
+ bool isBadRepresentative( Node n );
+ public:
+ InfRepModel( TypeNode tn, context::Context* c, TheoryUF* th ) : RepModel( tn ),
+ d_th( th ), d_rep( c ), d_const_rep( c ){}
+ virtual ~InfRepModel(){}
+ /** initialize */
+ void initialize( OutputChannel* out );
+ /** new node */
+ void newEqClass( Node n );
+ /** merge */
+ void merge( Node a, Node b );
+ /** assert terms are disequal */
+ void assertDisequal( Node a, Node b, Node reason ){}
+ /** check */
+ void check( Theory::Effort level, OutputChannel* out );
+ /** minimize */
+ bool minimize( OutputChannel* out );
+ /** get representatives */
+ void getRepresentatives( std::vector< Node >& reps );
+ /** print debug */
+ void debugPrint( const char* c ){}
+ };
private:
/** The output channel for the strong solver. */
OutputChannel* d_out;
/** theory uf pointer */
TheoryUF* d_th;
- /** conflict find structure, one for each type */
- std::map< TypeNode, ConflictFind* > d_conf_find;
+ /** Are we in conflict */
+ context::CDO<bool> d_conflict;
+ /** rep model structure, one for each type */
+ std::map< TypeNode, RepModel* > d_rep_model;
/** all types */
std::vector< TypeNode > d_conf_types;
/** whether conflict find data structures have been initialized */
- TypeNodeBoolMap d_conf_find_init;
- /** pre register type */
- void preRegisterType( TypeNode tn );
+ TypeNodeBoolMap d_rep_model_init;
/** get conflict find */
- ConflictFind* getConflictFind( TypeNode tn );
+ RepModel* getRepModel( Node n );
+private:
+ /** term disambiguator */
+ TermDisambiguator* d_term_amb;
public:
StrongSolverTheoryUf(context::Context* c, context::UserContext* u, OutputChannel& out, TheoryUF* th);
~StrongSolverTheoryUf() {}
@@ -279,6 +364,8 @@ public:
void check( Theory::Effort level );
/** propagate */
void propagate( Theory::Effort level );
+ /** get next decision request */
+ Node getNextDecisionRequest();
/** preregister a term */
void preRegisterTerm( TNode n );
/** preregister a quantifier */
@@ -290,35 +377,52 @@ public:
std::string identify() const { return std::string("StrongSolverTheoryUf"); }
//print debug
void debugPrint( const char* c );
+ /** debug a model */
+ void debugModel( TheoryModel* m );
public:
/** get number of types */
int getNumCardinalityTypes() { return (int)d_conf_types.size(); }
/** get type */
TypeNode getCardinalityType( int i ) { return d_conf_types[i]; }
+ /** get is in conflict */
+ bool isConflict() { return d_conflict; }
/** get cardinality for sort */
- int getCardinality( TypeNode t );
+ int getCardinality( Node n );
/** get representatives */
- void getRepresentatives( TypeNode t, std::vector< Node >& reps );
- /** get cardinality term */
- //Node getCardinalityTerm( TypeNode t );
+ void getRepresentatives( Node n, std::vector< Node >& reps );
/** minimize */
- bool minimize();
+ bool minimize( TheoryModel* m = NULL );
class Statistics {
public:
IntStat d_clique_lemmas;
IntStat d_split_lemmas;
IntStat d_disamb_term_lemmas;
+ IntStat d_totality_lemmas;
IntStat d_max_model_size;
Statistics();
~Statistics();
};
/** statistics class */
Statistics d_statistics;
+};/* class StrongSolverTheoryUf */
+
+class TermDisambiguator
+{
+private:
+ /** quantifiers engine */
+ QuantifiersEngine* d_qe;
+ /** whether two terms are ambiguous (indexed by equalities) */
+ context::CDHashMap<Node, bool, NodeHashFunction> d_term_amb;
/** involves relevant type */
static bool involvesRelevantType( Node n );
-};/* class StrongSolverTheoryUf */
+public:
+ TermDisambiguator( QuantifiersEngine* qe, context::Context* c ) : d_qe( qe ), d_term_amb( c ){}
+ ~TermDisambiguator(){}
+ /** check ambiguous terms */
+ int disambiguateTerms( OutputChannel* out );
+};
}
}/* CVC4::theory namespace */
diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h
index d00b69398..09f287884 100644
--- a/src/theory/uf/theory_uf_type_rules.h
+++ b/src/theory/uf/theory_uf_type_rules.h
@@ -72,68 +72,6 @@ public:
}
};/* class CardinalityConstraintTypeRule */
-class FunctionModelTypeRule {
-public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
- throw(TypeCheckingExceptionPrivate) {
- TypeNode tn = n[0].getType(check);
- if( check ){
- if( n.getNumChildren()==2 ){
- if( n[0].getKind()!=kind::FUNCTION_CASE_SPLIT ){
- throw TypeCheckingExceptionPrivate(n, "improper function model representation : first child must be case split");
- }
- TypeNode tn2 = n[1].getType(check);
- if( tn!=tn2 ){
- std::stringstream ss;
- ss << "function model has inconsistent return types : " << tn << " " << tn2;
- throw TypeCheckingExceptionPrivate(n, ss.str());
- }
- }
- }
- return tn;
- }
-};/* class FunctionModelTypeRule */
-
-class FunctionCaseSplitTypeRule {
-public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
- throw(TypeCheckingExceptionPrivate) {
- TypeNode retType = n[0][1].getType(check);
- if( check ){
- TypeNode argType = n[0][0].getType(check);
- for( size_t i=0; i<n.getNumChildren(); i++ ){
- TypeNode argType2 = n[i][0].getType(check);
- if( argType!=argType2 ){
- std::stringstream ss;
- ss << "function case split has inconsistent argument types : " << argType << " " << argType2;
- throw TypeCheckingExceptionPrivate(n, ss.str());
- }
- TypeNode retType2 = n[i][1].getType(check);
- if( retType!=retType2 ){
- std::stringstream ss;
- ss << "function case split has inconsistent return types : " << retType << " " << retType2;
- throw TypeCheckingExceptionPrivate(n, ss.str());
- }
- }
- }
- return retType;
- }
-};/* class FunctionCaseSplitTypeRule */
-
-
-class FunctionCaseTypeRule {
-public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
- throw(TypeCheckingExceptionPrivate) {
- TypeNode retType = n[1].getType(check);
- if( check ){
- TypeNode argType = n[0].getType(check);
- }
- return retType;
- }
-};/* class FunctionCaseTypeRule */
-
-
}/* CVC4::theory::uf namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback