summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/printer/cvc/cvc_printer.cpp53
-rw-r--r--src/printer/smt2/smt2_printer.cpp46
-rw-r--r--src/smt/options2
-rw-r--r--src/theory/arrays/theory_arrays_rewriter.h11
-rw-r--r--src/theory/quantifiers/inst_match.cpp12
-rw-r--r--src/theory/quantifiers/inst_match.h2
-rw-r--r--src/theory/quantifiers/instantiation_engine.cpp22
-rw-r--r--src/theory/quantifiers/model_engine.cpp5
-rw-r--r--src/theory/quantifiers/options2
-rw-r--r--src/theory/quantifiers/term_database.cpp8
-rw-r--r--src/theory/quantifiers_engine.cpp94
-rw-r--r--src/theory/quantifiers_engine.h9
-rw-r--r--src/theory/rep_set.cpp13
-rw-r--r--src/theory/uf/options2
-rw-r--r--src/theory/uf/theory_uf.cpp12
-rw-r--r--src/theory/uf/theory_uf.h8
-rw-r--r--src/theory/uf/theory_uf_strong_solver.cpp416
-rw-r--r--src/theory/uf/theory_uf_strong_solver.h117
18 files changed, 506 insertions, 328 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index e0d4656f4..0206c4252 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -21,7 +21,9 @@
#include "expr/command.h"
#include "theory/substitutions.h"
#include "smt/smt_engine.h"
+#include "smt/options.h"
#include "theory/model.h"
+#include "theory/arrays/theory_arrays_rewriter.h"
#include <iostream>
#include <vector>
@@ -813,21 +815,34 @@ void CvcPrinter::toStream(std::ostream& out, Model& m, const Command* c) const t
theory::TheoryModel& tm = (theory::TheoryModel&) m;
if(dynamic_cast<const DeclareTypeCommand*>(c) != NULL) {
TypeNode tn = TypeNode::fromType( ((const DeclareTypeCommand*)c)->getType() );
- if( tn.isSort() ){
- // print the cardinality
- if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
- out << "; cardinality of " << tn << " is " << (*tm.d_rep_set.d_type_reps.find(tn)).second.size() << std::endl;
+ if( options::modelUninterpDtEnum() && tn.isSort() &&
+ tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
+ out << "DATATYPE " << std::endl;
+ out << " " << dynamic_cast<const DeclareTypeCommand*>(c)->getSymbol() << " = ";
+ for( size_t i=0; i<(*tm.d_rep_set.d_type_reps.find(tn)).second.size(); i++ ){
+ if (i>0) {
+ out << "| ";
+ }
+ out << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << " ";
}
- }
- out << c << std::endl;
- if( tn.isSort() ){
- // print the representatives
- if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
- for( size_t i=0; i<(*tm.d_rep_set.d_type_reps.find(tn)).second.size(); i++ ){
- if( (*tm.d_rep_set.d_type_reps.find(tn)).second[i].isVar() ){
- out << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << " : " << tn << ";" << std::endl;
- }else{
- out << "% rep: " << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << std::endl;
+ out << std::endl << "END;" << std::endl;
+ } else {
+ if( tn.isSort() ){
+ // print the cardinality
+ if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
+ out << "% cardinality of " << tn << " is " << (*tm.d_rep_set.d_type_reps.find(tn)).second.size() << std::endl;
+ }
+ }
+ out << c << std::endl;
+ if( tn.isSort() ){
+ // print the representatives
+ if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
+ for( size_t i=0; i<(*tm.d_rep_set.d_type_reps.find(tn)).second.size(); i++ ){
+ if( (*tm.d_rep_set.d_type_reps.find(tn)).second[i].isVar() ){
+ out << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << " : " << tn << ";" << std::endl;
+ }else{
+ out << "% rep: " << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << std::endl;
+ }
}
}
}
@@ -850,7 +865,15 @@ void CvcPrinter::toStream(std::ostream& out, Model& m, const Command* c) const t
}else{
out << tn;
}
- out << " = " << Node::fromExpr(tm.getSmtEngine()->getValue(n.toExpr())) << ";" << std::endl;
+ Node val = Node::fromExpr(tm.getSmtEngine()->getValue(n.toExpr()));
+ if( options::modelUninterpDtEnum() && val.getKind() == kind::STORE ) {
+ TypeNode tn = val[1].getType();
+ if (tn.isSort() && tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
+ Cardinality indexCard((*tm.d_rep_set.d_type_reps.find(tn)).second.size());
+ val = theory::arrays::TheoryArraysRewriter::normalizeConstant( val, indexCard );
+ }
+ }
+ out << " = " << val << ";" << std::endl;
/*
//for table format (work in progress)
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 000fd2fbf..8541ca6ae 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -27,8 +27,10 @@
#include "theory/substitutions.h"
#include "util/language.h"
#include "smt/smt_engine.h"
+#include "smt/options.h"
#include "theory/model.h"
+#include "theory/arrays/theory_arrays_rewriter.h"
using namespace std;
@@ -552,21 +554,30 @@ void Smt2Printer::toStream(std::ostream& out, Model& m, const Command* c) const
theory::TheoryModel& tm = (theory::TheoryModel&) m;
if(dynamic_cast<const DeclareTypeCommand*>(c) != NULL) {
TypeNode tn = TypeNode::fromType( ((const DeclareTypeCommand*)c)->getType() );
- if( tn.isSort() ){
- //print the cardinality
- if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
- out << "; cardinality of " << tn << " is " << (*tm.d_rep_set.d_type_reps.find(tn)).second.size() << std::endl;
+ if( options::modelUninterpDtEnum() && tn.isSort() &&
+ tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
+ out << "(declare-datatypes () ((" << dynamic_cast<const DeclareTypeCommand*>(c)->getSymbol() << " ";
+ for( size_t i=0; i<(*tm.d_rep_set.d_type_reps.find(tn)).second.size(); i++ ){
+ out << "(" << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << ")";
}
- }
- out << c << std::endl;
- if( tn.isSort() ){
- //print the representatives
- if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
- for( size_t i=0; i<(*tm.d_rep_set.d_type_reps.find(tn)).second.size(); i++ ){
- if( (*tm.d_rep_set.d_type_reps.find(tn)).second[i].isVar() ){
- out << "(declare-fun " << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << " () " << tn << ")" << std::endl;
- }else{
- out << "; rep: " << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << std::endl;
+ out << ")))" << std::endl;
+ } else {
+ if( tn.isSort() ){
+ //print the cardinality
+ if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
+ out << "; cardinality of " << tn << " is " << (*tm.d_rep_set.d_type_reps.find(tn)).second.size() << std::endl;
+ }
+ }
+ out << c << std::endl;
+ if( tn.isSort() ){
+ //print the representatives
+ if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
+ for( size_t i=0; i<(*tm.d_rep_set.d_type_reps.find(tn)).second.size(); i++ ){
+ if( (*tm.d_rep_set.d_type_reps.find(tn)).second[i].isVar() ){
+ out << "(declare-fun " << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << " () " << tn << ")" << std::endl;
+ }else{
+ out << "; rep: " << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << std::endl;
+ }
}
}
}
@@ -583,6 +594,13 @@ void Smt2Printer::toStream(std::ostream& out, Model& m, const Command* c) const
<< " " << n.getType().getRangeType()
<< " " << val[1] << ")" << std::endl;
} else {
+ if( options::modelUninterpDtEnum() && val.getKind() == kind::STORE ) {
+ TypeNode tn = val[1].getType();
+ if (tn.isSort() && tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
+ Cardinality indexCard((*tm.d_rep_set.d_type_reps.find(tn)).second.size());
+ val = theory::arrays::TheoryArraysRewriter::normalizeConstant( val, indexCard );
+ }
+ }
out << "(define-fun " << n << " () "
<< n.getType() << " " << val << ")" << std::endl;
}
diff --git a/src/smt/options b/src/smt/options
index fc5ccf4c4..2680f4105 100644
--- a/src/smt/options
+++ b/src/smt/options
@@ -54,6 +54,8 @@ common-option incrementalSolving incremental -i --incremental bool
option abstractValues abstract-values --abstract-values bool :default false
in models, output arrays (and in future, maybe others) using abstract values, as required by the SMT-LIB standard
+option modelUninterpDtEnum --model-u-dt-enum bool :default false
+ in models, output uninterpreted sorts as datatype enumerations
option - regular-output-channel argument :handler CVC4::smt::setRegularOutputChannel :handler-include "smt/options_handlers.h"
set the regular output channel of the solver
diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h
index da479616d..9cbb0c9e8 100644
--- a/src/theory/arrays/theory_arrays_rewriter.h
+++ b/src/theory/arrays/theory_arrays_rewriter.h
@@ -37,8 +37,12 @@ typedef expr::Attribute<attr::ArrayConstantMostFrequentValueCountTag, uint64_t>
typedef expr::Attribute<attr::ArrayConstantMostFrequentValueTag, Node> ArrayConstantMostFrequentValueAttr;
class TheoryArraysRewriter {
-
static Node normalizeConstant(TNode node) {
+ return normalizeConstant(node, node[1].getType().getCardinality());
+ }
+public:
+ //this function is called by printers when using the option "--model-u-dt-enum"
+ static Node normalizeConstant(TNode node, Cardinality indexCard) {
TNode store = node[0];
TNode index = node[1];
TNode value = node[2];
@@ -112,7 +116,6 @@ class TheoryArraysRewriter {
return n;
}
- Cardinality indexCard = index.getType().getCardinality();
if (indexCard.isInfinite()) {
return n;
}
@@ -189,13 +192,15 @@ class TheoryArraysRewriter {
std::vector<Node> newIndices;
TypeEnumerator te(index.getType());
bool needToSort = false;
- while (!te.isFinished()) {
+ unsigned numTe = 0;
+ while (!te.isFinished() && (!indexCard.isFinite() || numTe<indexCard.getFiniteCardinality().toUnsignedInt())) {
if (indexSet.find(*te) == indexSet.end()) {
if (!newIndices.empty() && (!(newIndices.back() < (*te)))) {
needToSort = true;
}
newIndices.push_back(*te);
}
+ ++numTe;
++te;
}
Assert(indexCard.compare(newIndices.size() + depth) == Cardinality::EQUAL);
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index dcd7a1b79..85a96f90a 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -103,12 +103,12 @@ void InstMatch::makeComplete( Node f, QuantifiersEngine* qe ){
}
}
-void InstMatch::makeInternalRepresentative( QuantifiersEngine* qe ){
- EqualityQueryQuantifiersEngine* eqqe = (EqualityQueryQuantifiersEngine*)qe->getEqualityQuery();
- for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){
- d_map[ it->first ] = eqqe->getInternalRepresentative( it->second );
- }
-}
+//void InstMatch::makeInternalRepresentative( QuantifiersEngine* qe ){
+// EqualityQueryQuantifiersEngine* eqqe = (EqualityQueryQuantifiersEngine*)qe->getEqualityQuery();
+// for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){
+// d_map[ it->first ] = eqqe->getInternalRepresentative( it->second );
+// }
+//}
void InstMatch::makeRepresentative( QuantifiersEngine* qe ){
for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index 8b2d9726b..b9e61be20 100644
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -58,7 +58,7 @@ public:
/** make complete */
void makeComplete( Node f, QuantifiersEngine* qe );
/** make internal representative */
- void makeInternalRepresentative( QuantifiersEngine* qe );
+ //void makeInternalRepresentative( QuantifiersEngine* qe );
/** make representative */
void makeRepresentative( QuantifiersEngine* qe );
/** get value */
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 53977ee4f..75cc10615 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -84,16 +84,18 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
//add cbqi lemma
//get the counterexample literal
Node ceLit = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( f );
- //require any decision on cel to be phase=true
- d_quantEngine->getOutputChannel().requirePhase( ceLit, true );
- Debug("cbqi-debug") << "Require phase " << ceLit << " = true." << std::endl;
- //add counterexample lemma
- NodeBuilder<> nb(kind::OR);
- nb << f << ceLit;
- Node lem = nb;
- Debug("cbqi-debug") << "Counterexample lemma : " << lem << std::endl;
- d_quantEngine->getOutputChannel().lemma( lem );
- addedLemma = true;
+ if( !ceLit.isNull() ){
+ //require any decision on cel to be phase=true
+ d_quantEngine->getOutputChannel().requirePhase( ceLit, true );
+ Debug("cbqi-debug") << "Require phase " << ceLit << " = true." << std::endl;
+ //add counterexample lemma
+ NodeBuilder<> nb(kind::OR);
+ nb << f << ceLit;
+ Node lem = nb;
+ Debug("cbqi-debug") << "Counterexample lemma : " << lem << std::endl;
+ d_quantEngine->getOutputChannel().lemma( lem );
+ addedLemma = true;
+ }
}
}
if( addedLemma ){
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index bf6ea11f0..39377d11c 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -73,9 +73,8 @@ void ModelEngine::check( Theory::Effort e ){
if( addedLemmas==0 ){
Trace("model-engine-debug") << "Verify uf ss is minimal..." << std::endl;
//let the strong solver verify that the model is minimal
- uf::StrongSolverTheoryUf* uf_ss = ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver();
//for debugging, this will if there are terms in the model that the strong solver was not notified of
- uf_ss->debugModel( fm );
+ ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->debugModel( fm );
Trace("model-engine-debug") << "Check model..." << std::endl;
d_incomplete_check = false;
//print debug
@@ -164,7 +163,7 @@ int ModelEngine::checkModel( int checkOption ){
Trace("model-engine-debug") << " ";
for( size_t i=0; i<it->second.size(); i++ ){
//Trace("model-engine-debug") << it->second[i] << " ";
- Node r = ((EqualityQueryQuantifiersEngine*)d_quantEngine->getEqualityQuery())->getInternalRepresentative( it->second[i] );
+ Node r = ((EqualityQueryQuantifiersEngine*)d_quantEngine->getEqualityQuery())->getRepresentative( it->second[i] );
Trace("model-engine-debug") << r << " ";
}
Trace("model-engine-debug") << std::endl;
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index eace177b7..6b204eb60 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -71,7 +71,7 @@ option userPatternsQuant /--ignore-user-patterns bool :default true
option flipDecision --flip-decision/ bool :default false
turns on flip decision heuristic
-option internalReps --disable-quant-internal-reps/ bool :default true
+option internalReps /--disable-quant-internal-reps bool :default true
disables instantiating with representatives chosen by quantifiers engine
option finiteModelFind --finite-model-find bool :default false
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 78109ea37..65624686a 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -338,6 +338,14 @@ Node TermDb::getInstConstantBody( Node f ){
Node TermDb::getCounterexampleLiteral( Node f ){
if( d_ce_lit.find( f )==d_ce_lit.end() ){
Node ceBody = getInstConstantBody( f );
+ //check if any variable are of bad types, and fail if so
+ for( size_t i=0; i<d_inst_constants[f].size(); i++ ){
+ if( d_inst_constants[f][i].getType().isBoolean() ){
+ d_ce_lit[ f ] = Node::null();
+ return Node::null();
+ }
+ }
+ //otherwise, ensure literal
Node ceLit = d_quantEngine->getValuation().ensureLiteral( ceBody.notNode() );
d_ce_lit[ f ] = ceLit;
setInstantiationConstantAttr( ceLit, f );
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index f938199f8..50433facd 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -371,7 +371,7 @@ bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool modEq, bool
//make it representative, this is helpful for recognizing duplication
if( mkRep ){
//pick the best possible representative for instantiation, based on past use and simplicity of term
- Node r = d_eq_query->getInternalRepresentative( val );
+ Node r = d_eq_query->getInternalRepresentative( val, f, i );
Trace("inst-add-debug") << "mkRep " << r << " " << val << std::endl;
m.set( ic, r );
}
@@ -477,56 +477,6 @@ void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){
d_statistics.d_lit_phase_nreq += (int)nodes.size();
}
}
-/*
-EqualityQuery* QuantifiersEngine::getEqualityQuery(TypeNode t) {
- // Should use skeleton (in order to have the type and the kind
- // or any needed other information) instead of only the type
-
- // TheoryId id = Theory::theoryOf(t);
- // inst::EqualityQuery* eq = d_eq_query_arr[id];
- // if(eq == NULL) return d_eq_query_arr[theory::THEORY_UF];
- // else return eq;
-
- // hack because the generic one is too slow
- // TheoryId id = Theory::theoryOf(t);
- // if( true || id == theory::THEORY_UF){
- // uf::InstantiatorTheoryUf* ith = static_cast<uf::InstantiatorTheoryUf*>( getInstantiator( theory::THEORY_UF ));
- // return new uf::EqualityQueryInstantiatorTheoryUf(ith);
- // }
- // inst::EqualityQuery* eq = d_eq_query_arr[id];
- // if(eq == NULL) return d_eq_query_arr[theory::THEORY_UF];
- // else return eq;
-
-
- //Currently we use the generic EqualityQuery
- return getEqualityQuery();
-}
-
-
-rrinst::CandidateGenerator* QuantifiersEngine::getRRCanGenClasses() {
- return new GenericCandidateGeneratorClasses(this);
-}
-
-rrinst::CandidateGenerator* QuantifiersEngine::getRRCanGenClass() {
- return new GenericCandidateGeneratorClass(this);
-}
-
-rrinst::CandidateGenerator* QuantifiersEngine::getRRCanGenClasses(TypeNode t) {
- // TheoryId id = Theory::theoryOf(t);
- // rrinst::CandidateGenerator* eq = getInstantiator(id)->getRRCanGenClasses();
- // if(eq == NULL) return getInstantiator(id)->getRRCanGenClasses();
- // else return eq;
- return getRRCanGenClasses();
-}
-
-rrinst::CandidateGenerator* QuantifiersEngine::getRRCanGenClass(TypeNode t) {
- // TheoryId id = Theory::theoryOf(t);
- // rrinst::CandidateGenerator* eq = getInstantiator(id)->getRRCanGenClass();
- // if(eq == NULL) return getInstantiator(id)->getRRCanGenClass();
- // else return eq;
- return getRRCanGenClass();
-}
-*/
QuantifiersEngine::Statistics::Statistics():
d_num_quant("QuantifiersEngine::Num_Quantifiers", 0),
@@ -652,39 +602,57 @@ bool EqualityQueryQuantifiersEngine::areDisequal( Node a, Node b ){
return false;
}
-Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a ){
+Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, int index ){
Node r = getRepresentative( a );
if( !options::internalReps() ){
return r;
}else{
- if( d_int_rep.find( r )==d_int_rep.end() ){
+ int sortId = 0;
+ if( optInternalRepSortInference() ){
+ sortId = d_qe->getTheoryEngine()->getSortInference()->getSortId( f, f[0][index] );
+ }
+ if( d_int_rep[sortId].find( r )==d_int_rep[sortId].end() ){
std::vector< Node > eqc;
getEquivalenceClass( r, eqc );
//find best selection for representative
- Node r_best = r;
- int r_best_score = getRepScore( r );
+ Node r_best;
+ int r_best_score;
for( size_t i=0; i<eqc.size(); i++ ){
- int score = getRepScore( eqc[i] );
+ int score = getRepScore( eqc[i], f, index );
+ if( optInternalRepSortInference() ){
+ int e_sortId = d_qe->getTheoryEngine()->getSortInference()->getSortId( eqc[i]);
+ if( score>=0 && e_sortId!=sortId ){
+ score += 100;
+ }
+ }
//score prefers earliest use of this term as a representative
- if( score>=0 && ( r_best_score<0 || score<r_best_score ) ){
+ if( r_best.isNull() || ( score>=0 && ( r_best_score<0 || score<r_best_score ) ) ){
r_best = eqc[i];
r_best_score = score;
}
}
//now, make sure that no other member of the class is an instance
- r_best = getInstance( r_best, eqc );
+ if( !optInternalRepSortInference() ){
+ r_best = getInstance( r_best, eqc );
+ }
//store that this representative was chosen at this point
if( d_rep_score.find( r_best )==d_rep_score.end() ){
d_rep_score[ r_best ] = d_reset_count;
}
- d_int_rep[r] = r_best;
+ d_int_rep[sortId][r] = r_best;
if( r_best!=a ){
Trace("internal-rep-debug") << "rep( " << a << " ) = " << r << ", " << std::endl;
Trace("internal-rep-debug") << "int_rep( " << a << " ) = " << r_best << ", " << std::endl;
}
+ if( optInternalRepSortInference() ){
+ int sortIdBest = d_qe->getTheoryEngine()->getSortInference()->getSortId( r_best );
+ if( sortId!=sortIdBest ){
+ Trace("sort-inf-rep") << "Choosing representative with bad type " << r_best << " " << sortId << " " << sortIdBest << std::endl;
+ }
+ }
return r_best;
}else{
- return d_int_rep[r];
+ return d_int_rep[sortId][r];
}
}
}
@@ -740,7 +708,11 @@ int getDepth( Node n ){
}
}
-int EqualityQueryQuantifiersEngine::getRepScore( Node n ){
+int EqualityQueryQuantifiersEngine::getRepScore( Node n, Node f, int index ){
return d_rep_score.find( n )==d_rep_score.end() ? -1 : d_rep_score[n]; //initial
//return ( d_rep_score.find( n )==d_rep_score.end() ? 100 : 0 ) + getDepth( n ); //term depth
}
+
+bool EqualityQueryQuantifiersEngine::optInternalRepSortInference() {
+ return false;
+} \ No newline at end of file
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index fa8a51d1f..9f520f420 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -214,6 +214,7 @@ public:
rrinst::TriggerTrie* getRRTriggerDatabase() { return d_rr_tr_trie; }
/** add term to database */
void addTermToDatabase( Node n, bool withinQuant = false );
+ /** get the master equality engine */
eq::EqualityEngine* getMasterEqualityEngine() ;
public:
/** statistics class */
@@ -266,7 +267,7 @@ private:
/** pointer to theory engine */
QuantifiersEngine* d_qe;
/** internal representatives */
- std::map< Node, Node > d_int_rep;
+ std::map< int, std::map< Node, Node > > d_int_rep;
/** rep score */
std::map< Node, int > d_rep_score;
/** reset count */
@@ -275,7 +276,9 @@ private:
/** node contains */
Node getInstance( Node n, std::vector< Node >& eqc );
/** get score */
- int getRepScore( Node n );
+ int getRepScore( Node n, Node f, int index );
+ /** choose rep based on sort inference */
+ bool optInternalRepSortInference();
public:
EqualityQueryQuantifiersEngine( QuantifiersEngine* qe ) : d_qe( qe ), d_reset_count( 0 ){}
~EqualityQueryQuantifiersEngine(){}
@@ -292,7 +295,7 @@ public:
If cbqi is active, this will return a term in the equivalence class of "a" that does
not contain instantiation constants, if such a term exists.
*/
- Node getInternalRepresentative( Node a );
+ Node getInternalRepresentative( Node a, Node f, int index );
}; /* EqualityQueryQuantifiersEngine */
}/* CVC4::theory namespace */
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index 4ae7f2d0c..2df0c3f61 100644
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -135,16 +135,9 @@ bool RepSetIterator::initialize(){
}else if( tn.isInteger() || tn.isReal() ){
Trace("fmf-incomplete") << "Incomplete because of infinite type " << tn << std::endl;
d_incomplete = true;
- }else if( tn.isDatatype() ){
- const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
- //if finite, then complete all values of the domain
- if( dt.isFinite() ){
- d_rep_set->complete( tn );
- //d_incomplete = true;
- }else{
- Trace("fmf-incomplete") << "Incomplete because of infinite datatype " << tn << std::endl;
- d_incomplete = true;
- }
+ //enumerate if the sort is reasonably small, the upper bound of 128 is chosen arbitrarily for now
+ }else if( tn.getCardinality().isFinite() && tn.getCardinality().getFiniteCardinality().toUnsignedInt()<=128 ){
+ d_rep_set->complete( tn );
}else{
Trace("fmf-incomplete") << "Incomplete because of unknown type " << tn << std::endl;
d_incomplete = true;
diff --git a/src/theory/uf/options b/src/theory/uf/options
index d6a2bb025..33d1255ef 100644
--- a/src/theory/uf/options
+++ b/src/theory/uf/options
@@ -28,5 +28,7 @@ option ufssExplainedCliques --uf-ss-explained-cliques bool :default false
use explained clique lemmas for uf strong solver
option ufssSimpleCliques --uf-ss-simple-cliques bool :default true
always use simple clique lemmas for uf strong solver
+option ufssDiseqPropagation --uf-ss-deq-prop bool :default false
+ eagerly propagate disequalities for uf strong solver
endmodule
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 3f033f3b8..bdbb79195 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -33,7 +33,7 @@ TheoryUF::TheoryUF(context::Context* c, context::UserContext* u, OutputChannel&
d_notify(*this),
/* The strong theory solver can be notified by EqualityEngine::init(),
* so make sure it's initialized first. */
- d_thss(options::finiteModelFind() ? new StrongSolverTheoryUf(c, u, out, this) : NULL),
+ d_thss(options::finiteModelFind() ? new StrongSolverTheoryUF(c, u, out, this) : NULL),
d_equalityEngine(d_notify, c, "theory::uf::TheoryUF"),
d_conflict(c, false),
d_literalsToPropagate(c),
@@ -101,12 +101,10 @@ void TheoryUF::check(Effort level) {
}
- if (d_thss != NULL) {
- if (! d_conflict) {
- d_thss->check(level);
- if( d_thss->isConflict() ){
- d_conflict = true;
- }
+ if (d_thss != NULL && ! d_conflict) {
+ d_thss->check(level);
+ if( d_thss->isConflict() ){
+ d_conflict = true;
}
}
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index fe1fc5137..00e270bd0 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -35,11 +35,11 @@ namespace theory {
namespace uf {
class UfTermDb;
-class StrongSolverTheoryUf;
+class StrongSolverTheoryUF;
class TheoryUF : public Theory {
- friend class StrongSolverTheoryUf;
+ friend class StrongSolverTheoryUF;
public:
@@ -116,7 +116,7 @@ private:
NotifyClass d_notify;
/** The associated theory strong solver (or NULL if none) */
- StrongSolverTheoryUf* d_thss;
+ StrongSolverTheoryUF* d_thss;
/** Equaltity engine */
eq::EqualityEngine d_equalityEngine;
@@ -212,7 +212,7 @@ public:
return &d_equalityEngine;
}
- StrongSolverTheoryUf* getStrongSolver() {
+ StrongSolverTheoryUF* getStrongSolver() {
return d_thss;
}
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index 0a96cf548..3e31faedb 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -32,11 +32,11 @@ using namespace CVC4::context;
using namespace CVC4::theory;
using namespace CVC4::theory::uf;
-void StrongSolverTheoryUf::SortRepModel::Region::addRep( Node n ) {
+void StrongSolverTheoryUF::SortModel::Region::addRep( Node n ) {
setRep( n, true );
}
-void StrongSolverTheoryUf::SortRepModel::Region::takeNode( StrongSolverTheoryUf::SortRepModel::Region* r, Node n ){
+void StrongSolverTheoryUF::SortModel::Region::takeNode( StrongSolverTheoryUF::SortModel::Region* r, Node n ){
Assert( !hasRep( n ) );
Assert( r->hasRep( n ) );
//add representative
@@ -68,7 +68,7 @@ void StrongSolverTheoryUf::SortRepModel::Region::takeNode( StrongSolverTheoryUf:
r->setRep( n, false );
}
-void StrongSolverTheoryUf::SortRepModel::Region::combine( StrongSolverTheoryUf::SortRepModel::Region* r ){
+void StrongSolverTheoryUF::SortModel::Region::combine( StrongSolverTheoryUF::SortModel::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 ){
@@ -100,7 +100,7 @@ void StrongSolverTheoryUf::SortRepModel::Region::combine( StrongSolverTheoryUf::
}
/** setEqual */
-void StrongSolverTheoryUf::SortRepModel::Region::setEqual( Node a, Node b ){
+void StrongSolverTheoryUF::SortModel::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++ ){
@@ -108,10 +108,15 @@ void StrongSolverTheoryUf::SortRepModel::Region::setEqual( Node a, Node b ){
for( NodeBoolMap::iterator it = del->d_disequalities.begin(); it != del->d_disequalities.end(); ++it ){
if( (*it).second ){
Node n = (*it).first;
+ //get the region that contains the endpoint of the disequality b != ...
Region* nr = d_cf->d_regions[ d_cf->d_regions_map[ n ] ];
if( !isDisequal( a, n, t ) ){
setDisequal( a, n, t, true );
nr->setDisequal( n, a, t, true );
+ //notify the disequality propagator
+ if( options::ufssDiseqPropagation() ){
+ d_cf->d_thss->getDisequalityPropagator()->assertDisequal(a, n, Node::null());
+ }
}
setDisequal( b, n, t, false );
nr->setDisequal( n, b, t, false );
@@ -122,7 +127,7 @@ void StrongSolverTheoryUf::SortRepModel::Region::setEqual( Node a, Node b ){
setRep( b, false );
}
-void StrongSolverTheoryUf::SortRepModel::Region::setDisequal( Node n1, Node n2, int type, bool valid ){
+void StrongSolverTheoryUF::SortModel::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 );
@@ -148,10 +153,10 @@ void StrongSolverTheoryUf::SortRepModel::Region::setDisequal( Node n1, Node n2,
}
}
-void StrongSolverTheoryUf::SortRepModel::Region::setRep( Node n, bool valid ){
+void StrongSolverTheoryUF::SortModel::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() );
+ d_nodes[n] = new RegionNodeInfo( d_cf->d_thss->getSatContext() );
}
d_nodes[n]->d_valid = valid;
d_reps_size = d_reps_size + ( valid ? 1 : -1 );
@@ -172,24 +177,24 @@ void StrongSolverTheoryUf::SortRepModel::Region::setRep( Node n, bool valid ){
}
}
-bool StrongSolverTheoryUf::SortRepModel::Region::isDisequal( Node n1, Node n2, int type ){
+bool StrongSolverTheoryUF::SortModel::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::SortRepModel::Region* r;
+ StrongSolverTheoryUF::SortModel::Region* r;
bool operator() (Node i,Node j) { return (r->d_nodes[i]->getNumInternalDisequalities()>r->d_nodes[j]->getNumInternalDisequalities());}
};
struct sortExternalDegree {
- StrongSolverTheoryUf::SortRepModel::Region* r;
+ StrongSolverTheoryUF::SortModel::Region* r;
bool operator() (Node i,Node j) { return (r->d_nodes[i]->getNumExternalDisequalities()>r->d_nodes[j]->getNumExternalDisequalities());}
};
int gmcCount = 0;
-bool StrongSolverTheoryUf::SortRepModel::Region::getMustCombine( int cardinality ){
+bool StrongSolverTheoryUF::SortModel::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
@@ -228,7 +233,7 @@ bool StrongSolverTheoryUf::SortRepModel::Region::getMustCombine( int cardinality
return false;
}
-bool StrongSolverTheoryUf::SortRepModel::Region::check( Theory::Effort level, int cardinality, std::vector< Node >& clique ){
+bool StrongSolverTheoryUF::SortModel::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 ) ){
if( d_reps_size>1 ){
@@ -317,7 +322,7 @@ bool StrongSolverTheoryUf::SortRepModel::Region::check( Theory::Effort level, in
return false;
}
-void StrongSolverTheoryUf::SortRepModel::Region::getRepresentatives( std::vector< Node >& reps ){
+void StrongSolverTheoryUF::SortModel::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 ){
@@ -326,7 +331,7 @@ void StrongSolverTheoryUf::SortRepModel::Region::getRepresentatives( std::vector
}
}
-void StrongSolverTheoryUf::SortRepModel::Region::getNumExternalDisequalities( std::map< Node, int >& num_ext_disequalities ){
+void StrongSolverTheoryUF::SortModel::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 ){
@@ -340,7 +345,7 @@ void StrongSolverTheoryUf::SortRepModel::Region::getNumExternalDisequalities( st
}
}
-void StrongSolverTheoryUf::SortRepModel::Region::debugPrint( const char* c, bool incClique ){
+void StrongSolverTheoryUF::SortModel::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;
@@ -389,27 +394,27 @@ void StrongSolverTheoryUf::SortRepModel::Region::debugPrint( const char* c, bool
-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 ),
+StrongSolverTheoryUF::SortModel::SortModel( Node n, context::Context* c, StrongSolverTheoryUF* thss ) : d_type( n.getType() ),
+ d_thss( thss ), 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 ){
+void StrongSolverTheoryUF::SortModel::initialize( OutputChannel* out ){
allocateCardinality( out );
}
/** new node */
-void StrongSolverTheoryUf::SortRepModel::newEqClass( Node n ){
+void StrongSolverTheoryUF::SortModel::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() );
+ addTotalityAxiom( n, it->first, &d_thss->getOutputChannel() );
}
}
}
@@ -429,14 +434,14 @@ void StrongSolverTheoryUf::SortRepModel::newEqClass( Node n ){
if( options::ufssSmartSplits() ){
setSplitScore( n, 0 );
}
- Debug("uf-ss") << "StrongSolverTheoryUf: New Eq Class " << n << std::endl;
+ 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.push_back( new Region( this, d_thss->getSatContext() ) );
}
d_regions[ d_regions_index ]->addRep( n );
d_regions_index = d_regions_index + 1;
@@ -447,7 +452,7 @@ void StrongSolverTheoryUf::SortRepModel::newEqClass( Node n ){
}
/** merge */
-void StrongSolverTheoryUf::SortRepModel::merge( Node a, Node b ){
+void StrongSolverTheoryUF::SortModel::merge( Node a, Node b ){
if( !d_conflict ){
if( options::ufssTotality() ){
if( d_regions_map[b]==-1 ){
@@ -457,7 +462,7 @@ void StrongSolverTheoryUf::SortRepModel::merge( Node a, Node b ){
}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;
+ 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() );
@@ -495,21 +500,25 @@ void StrongSolverTheoryUf::SortRepModel::merge( Node a, Node b ){
d_regions_map[b] = -1;
}
d_reps = d_reps - 1;
- Debug("uf-ss") << "Done merge." << std::endl;
+
+ if( options::ufssDiseqPropagation() && !d_conflict ){
+ //notify the disequality propagator
+ d_thss->getDisequalityPropagator()->merge(a, b);
+ }
}
}
}
/** assert terms are disequal */
-void StrongSolverTheoryUf::SortRepModel::assertDisequal( Node a, Node b, Node reason ){
+void StrongSolverTheoryUF::SortModel::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 ) ){
+ a = d_thss->getTheory()->d_equalityEngine.getRepresentative( a );
+ b = d_thss->getTheory()->d_equalityEngine.getRepresentative( b );
+ if( !d_thss->getTheory()->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] ){
@@ -541,18 +550,34 @@ void StrongSolverTheoryUf::SortRepModel::assertDisequal( Node a, Node b, Node re
checkRegion( ai );
checkRegion( bi );
}
- //Notice() << "done" << std::endl;
+
+ if( options::ufssDiseqPropagation() && !d_conflict ){
+ //notify the disequality propagator
+ d_thss->getDisequalityPropagator()->assertDisequal(a, b, Node::null());
+ }
}
}
}
}
+bool StrongSolverTheoryUF::SortModel::areDisequal( Node a, Node b ) {
+ Assert( a == d_thss->getTheory()->d_equalityEngine.getRepresentative( a ) );
+ Assert( b == d_thss->getTheory()->d_equalityEngine.getRepresentative( b ) );
+ if( d_regions_map.find( a )!=d_regions_map.end() &&
+ d_regions_map.find( b )!=d_regions_map.end() ){
+ int ai = d_regions_map[a];
+ int bi = d_regions_map[b];
+ return d_regions[ai]->isDisequal(a, b, ai==bi ? 1 : 0);
+ }else{
+ return false;
+ }
+}
/** check */
-void StrongSolverTheoryUf::SortRepModel::check( Theory::Effort level, OutputChannel* out ){
+void StrongSolverTheoryUF::SortModel::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;
+ 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 ){
@@ -585,7 +610,7 @@ void StrongSolverTheoryUf::SortRepModel::check( Theory::Effort level, OutputChan
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() );
+ addTotalityAxiom( (*it).first, d_cardinality, &d_thss->getOutputChannel() );
}
}
}
@@ -620,7 +645,7 @@ void StrongSolverTheoryUf::SortRepModel::check( Theory::Effort level, OutputChan
for( int i=0; i<(int)d_regions_index; i++ ){
if( d_regions[i]->d_valid ){
Node op = d_regions[i]->d_nodes.begin()->first;
- int sort_id = d_th->getQuantifiersEngine()->getTheoryEngine()->getSortInference()->getSortId(op) ;
+ int sort_id = d_thss->getTheory()->getQuantifiersEngine()->getTheoryEngine()->getSortInference()->getSortId(op) ;
if( sortsFound.find( sort_id )!=sortsFound.end() ){
combineRegions( sortsFound[sort_id], i );
recheck = true;
@@ -651,11 +676,11 @@ void StrongSolverTheoryUf::SortRepModel::check( Theory::Effort level, OutputChan
}
}
-void StrongSolverTheoryUf::SortRepModel::propagate( Theory::Effort level, OutputChannel* out ){
+void StrongSolverTheoryUF::SortModel::propagate( Theory::Effort level, OutputChannel* out ){
}
-Node StrongSolverTheoryUf::SortRepModel::getNextDecisionRequest(){
+Node StrongSolverTheoryUF::SortModel::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 ){
@@ -670,7 +695,7 @@ Node StrongSolverTheoryUf::SortRepModel::getNextDecisionRequest(){
return Node::null();
}
-bool StrongSolverTheoryUf::SortRepModel::minimize( OutputChannel* out, TheoryModel* m ){
+bool StrongSolverTheoryUF::SortModel::minimize( OutputChannel* out, TheoryModel* m ){
if( options::ufssTotality() ){
//do nothing
}else{
@@ -692,7 +717,7 @@ bool StrongSolverTheoryUf::SortRepModel::minimize( OutputChannel* out, TheoryMod
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 );
+ ++( d_thss->d_statistics.d_split_lemmas );
return false;
}
}
@@ -726,7 +751,7 @@ bool StrongSolverTheoryUf::SortRepModel::minimize( OutputChannel* out, TheoryMod
}
-int StrongSolverTheoryUf::SortRepModel::getNumDisequalitiesToRegion( Node n, int ri ){
+int StrongSolverTheoryUF::SortModel::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];
@@ -740,7 +765,7 @@ int StrongSolverTheoryUf::SortRepModel::getNumDisequalitiesToRegion( Node n, int
return counter;
}
-void StrongSolverTheoryUf::SortRepModel::getDisequalitiesToRegions( int ri, std::map< int, int >& regions_diseq ){
+void StrongSolverTheoryUF::SortModel::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 ){
@@ -756,7 +781,7 @@ void StrongSolverTheoryUf::SortRepModel::getDisequalitiesToRegions( int ri, std:
}
}
-void StrongSolverTheoryUf::SortRepModel::setSplitScore( Node n, int s ){
+void StrongSolverTheoryUF::SortModel::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;
@@ -768,9 +793,10 @@ void StrongSolverTheoryUf::SortRepModel::setSplitScore( Node n, int s ){
}
}
-void StrongSolverTheoryUf::SortRepModel::assertCardinality( OutputChannel* out, int c, bool val ){
+void StrongSolverTheoryUF::SortModel::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;
+ Trace("uf-ss-assert") << "Assert cardinality " << d_type << " " << c << " " << val << " level = ";
+ Trace("uf-ss-assert") << d_thss->getTheory()->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 ){
@@ -823,7 +849,7 @@ void StrongSolverTheoryUf::SortRepModel::assertCardinality( OutputChannel* out,
}
}
-void StrongSolverTheoryUf::SortRepModel::checkRegion( int ri, bool checkCombine ){
+void StrongSolverTheoryUF::SortModel::checkRegion( int ri, bool checkCombine ){
if( isValid(ri) && d_hasCard ){
Assert( d_cardinality>0 );
if( checkCombine && d_regions[ri]->getMustCombine( d_cardinality ) ){
@@ -845,12 +871,12 @@ void StrongSolverTheoryUf::SortRepModel::checkRegion( int ri, bool checkCombine
std::vector< Node > clique;
if( d_regions[ri]->check( Theory::EFFORT_STANDARD, d_cardinality, clique ) ){
//explain clique
- addCliqueLemma( clique, &d_th->getOutputChannel() );
+ addCliqueLemma( clique, &d_thss->getOutputChannel() );
}
}
}
-int StrongSolverTheoryUf::SortRepModel::forceCombineRegion( int ri, bool useDensity ){
+int StrongSolverTheoryUF::SortModel::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 ){
@@ -890,7 +916,7 @@ int StrongSolverTheoryUf::SortRepModel::forceCombineRegion( int ri, bool useDens
}
-int StrongSolverTheoryUf::SortRepModel::combineRegions( int ai, int bi ){
+int StrongSolverTheoryUF::SortModel::combineRegions( int ai, int bi ){
#ifdef COMBINE_REGIONS_SMALL_INTO_LARGE
if( d_regions[ai]->getNumReps()<d_regions[bi]->getNumReps() ){
return combineRegions( bi, ai );
@@ -910,7 +936,7 @@ int StrongSolverTheoryUf::SortRepModel::combineRegions( int ai, int bi ){
return ai;
}
-void StrongSolverTheoryUf::SortRepModel::moveNode( Node n, int ri ){
+void StrongSolverTheoryUF::SortModel::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 ) );
@@ -919,7 +945,7 @@ void StrongSolverTheoryUf::SortRepModel::moveNode( Node n, int ri ){
d_regions_map[n] = ri;
}
-void StrongSolverTheoryUf::SortRepModel::allocateCardinality( OutputChannel* out ){
+void StrongSolverTheoryUF::SortModel::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") ){
@@ -957,7 +983,7 @@ void StrongSolverTheoryUf::SortRepModel::allocateCardinality( OutputChannel* out
//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 );
+ d_thss->getOutputChannel().lemma( lem );
}
}
@@ -976,18 +1002,18 @@ void StrongSolverTheoryUf::SortRepModel::allocateCardinality( OutputChannel* out
//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 );
+ d_thss->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() );
+ addTotalityAxiom( (*it).first, d_aloc_cardinality, &d_thss->getOutputChannel() );
}
}
}
}
-bool StrongSolverTheoryUf::SortRepModel::addSplit( Region* r, OutputChannel* out ){
+bool StrongSolverTheoryUF::SortModel::addSplit( Region* r, OutputChannel* out ){
if( r->hasSplits() ){
Node s;
if( !options::ufssSmartSplits() ){
@@ -1019,7 +1045,7 @@ bool StrongSolverTheoryUf::SortRepModel::addSplit( Region* r, OutputChannel* out
Trace("uf-ss-lemma") << "*** Split on " << s << std::endl;
if( options::sortInference()) {
for( int i=0; i<2; i++ ){
- int si = d_th->getQuantifiersEngine()->getTheoryEngine()->getSortInference()->getSortId( s[i] );
+ int si = d_thss->getTheory()->getQuantifiersEngine()->getTheoryEngine()->getSortInference()->getSortId( s[i] );
Trace("uf-ss-split-si") << si << " ";
}
Trace("uf-ss-split-si") << std::endl;
@@ -1032,7 +1058,7 @@ bool StrongSolverTheoryUf::SortRepModel::addSplit( Region* r, OutputChannel* out
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 );
+ ++( d_thss->d_statistics.d_split_lemmas );
return true;
}else{
return false;
@@ -1040,7 +1066,7 @@ bool StrongSolverTheoryUf::SortRepModel::addSplit( Region* r, OutputChannel* out
}
-void StrongSolverTheoryUf::SortRepModel::addCliqueLemma( std::vector< Node >& clique, OutputChannel* out ){
+void StrongSolverTheoryUF::SortModel::addCliqueLemma( std::vector< Node >& clique, OutputChannel* out ){
Assert( d_hasCard );
Assert( d_cardinality>0 );
while( clique.size()>size_t(d_cardinality+1) ){
@@ -1051,15 +1077,15 @@ void StrongSolverTheoryUf::SortRepModel::addCliqueLemma( std::vector< Node >& cl
std::vector< Node > eqs;
for( int i=0; i<(int)clique.size(); i++ ){
for( int j=0; j<i; j++ ){
- Node r1 = d_th->d_equalityEngine.getRepresentative(clique[i]);
- Node r2 = d_th->d_equalityEngine.getRepresentative(clique[j]);
+ Node r1 = d_thss->getTheory()->d_equalityEngine.getRepresentative(clique[i]);
+ Node r2 = d_thss->getTheory()->d_equalityEngine.getRepresentative(clique[j]);
eqs.push_back( clique[i].eqNode( clique[j] ) );
}
}
eqs.push_back( d_cardinality_literal[ d_cardinality ].notNode() );
Node lem = NodeManager::currentNM()->mkNode( OR, eqs );
Trace("uf-ss-lemma") << "*** Add clique conflict " << lem << std::endl;
- ++( d_th->getStrongSolver()->d_statistics.d_clique_lemmas );
+ ++( d_thss->d_statistics.d_clique_lemmas );
out->lemma( lem );
}else{
//debugging information
@@ -1087,8 +1113,8 @@ void StrongSolverTheoryUf::SortRepModel::addCliqueLemma( std::vector< Node >& cl
std::map< Node, Node > cliqueRepMap;
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] );
+ Node r1 = d_thss->getTheory()->d_equalityEngine.getRepresentative( d_disequalities[i][0][0] );
+ Node r2 = d_thss->getTheory()->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() ){
@@ -1145,7 +1171,7 @@ void StrongSolverTheoryUf::SortRepModel::addCliqueLemma( std::vector< Node >& cl
Debug("uf-ss-cliques") << " = ";
//explain it2->first and prev
std::vector< TNode > expl;
- d_th->d_equalityEngine.explainEquality( it2->first, prev, true, expl );
+ d_thss->getTheory()->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] );
@@ -1172,7 +1198,7 @@ void StrongSolverTheoryUf::SortRepModel::addCliqueLemma( std::vector< Node >& cl
//Notice() << "*** Add clique conflict " << conflictNode << std::endl;
out->conflict( conflictNode );
d_conflict = true;
- ++( d_th->getStrongSolver()->d_statistics.d_clique_conflicts );
+ ++( d_thss->d_statistics.d_clique_conflicts );
}else{
Node conflictNode = conflict.size()==1 ? conflict[0] : NodeManager::currentNM()->mkNode( AND, conflict );
//add cardinality constraint
@@ -1184,14 +1210,14 @@ void StrongSolverTheoryUf::SortRepModel::addCliqueLemma( std::vector< Node >& cl
conflictNode = NodeManager::currentNM()->mkNode( IMPLIES, conflictNode, cardNode.notNode() );
Trace("uf-ss-lemma") << "*** Add clique lemma " << conflictNode << std::endl;
out->lemma( conflictNode );
- ++( d_th->getStrongSolver()->d_statistics.d_clique_lemmas );
+ ++( d_thss->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::SortRepModel::addTotalityAxiom( Node n, int cardinality, OutputChannel* out ){
+void StrongSolverTheoryUF::SortModel::addTotalityAxiom( Node n, int cardinality, OutputChannel* out ){
Node cardLit = d_cardinality_literal[ cardinality ];
std::vector< Node > eqs;
for( int i=0; i<cardinality; i++ ){
@@ -1201,25 +1227,25 @@ void StrongSolverTheoryUf::SortRepModel::addTotalityAxiom( Node n, int cardinali
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 );
+ d_thss->getOutputChannel().lemma( lem );
+ ++( d_thss->d_statistics.d_totality_lemmas );
}
/** apply totality */
-bool StrongSolverTheoryUf::SortRepModel::applyTotality( int cardinality ){
+bool StrongSolverTheoryUF::SortModel::applyTotality( int cardinality ){
return options::ufssTotality() || cardinality<=options::ufssTotalityLimited();
// || ( options::ufssModelInference() && !d_totality_terms[cardinality].empty() );
}
/** get totality lemma terms */
-Node StrongSolverTheoryUf::SortRepModel::getTotalityLemmaTerm( int cardinality, int i ){
+Node StrongSolverTheoryUF::SortModel::getTotalityLemmaTerm( int cardinality, int i ){
return d_totality_terms[0][i];
//}else{
// return d_totality_terms[cardinality][i];
//}
}
-void StrongSolverTheoryUf::SortRepModel::debugPrint( const char* c ){
+void StrongSolverTheoryUF::SortModel::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;
@@ -1244,7 +1270,7 @@ void StrongSolverTheoryUf::SortRepModel::debugPrint( const char* c ){
}
}
-void StrongSolverTheoryUf::SortRepModel::debugModel( TheoryModel* m ){
+void StrongSolverTheoryUF::SortModel::debugModel( TheoryModel* m ){
if( Trace.isOn("uf-ss-warn") ){
std::vector< Node > eqcs;
eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &m->d_equalityEngine );
@@ -1271,7 +1297,7 @@ void StrongSolverTheoryUf::SortRepModel::debugModel( TheoryModel* m ){
}
}
-int StrongSolverTheoryUf::SortRepModel::getNumRegions(){
+int StrongSolverTheoryUF::SortModel::getNumRegions(){
int count = 0;
for( int i=0; i<(int)d_regions_index; i++ ){
if( d_regions[i]->d_valid ){
@@ -1281,7 +1307,7 @@ int StrongSolverTheoryUf::SortRepModel::getNumRegions(){
return count;
}
-void StrongSolverTheoryUf::SortRepModel::getRepresentatives( std::vector< Node >& reps ){
+void StrongSolverTheoryUF::SortModel::getRepresentatives( std::vector< Node >& reps ){
//if( !options::ufssColoringSat() ){
bool foundRegion = false;
for( int i=0; i<(int)d_regions_index; i++ ){
@@ -1300,7 +1326,7 @@ void StrongSolverTheoryUf::SortRepModel::getRepresentatives( std::vector< Node >
//}
}
-StrongSolverTheoryUf::StrongSolverTheoryUf(context::Context* c, context::UserContext* u, OutputChannel& out, TheoryUF* th) :
+StrongSolverTheoryUF::StrongSolverTheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, TheoryUF* th) :
d_out( &out ),
d_th( th ),
d_conflict( c, false ),
@@ -1313,74 +1339,118 @@ d_rep_model_init( c )
}else{
d_term_amb = NULL;
}
+ if( options::ufssDiseqPropagation() ){
+ d_deq_prop = new DisequalityPropagator( th->getQuantifiersEngine(), this );
+ }else{
+ d_deq_prop = NULL;
+ }
+}
+
+/** get default sat context */
+context::Context* StrongSolverTheoryUF::getSatContext() {
+ return d_th->getSatContext();
+}
+
+/** get default output channel */
+OutputChannel& StrongSolverTheoryUF::getOutputChannel() {
+ return d_th->getOutputChannel();
}
/** new node */
-void StrongSolverTheoryUf::newEqClass( Node n ){
- RepModel* c = getRepModel( n );
+void StrongSolverTheoryUF::newEqClass( Node n ){
+ SortModel* c = getSortModel( n );
if( c ){
- Trace("uf-ss-solver") << "StrongSolverTheoryUf: New eq class " << n << " : " << n.getType() << std::endl;
+ Trace("uf-ss-solver") << "StrongSolverTheoryUF: New eq class " << n << " : " << n.getType() << std::endl;
c->newEqClass( n );
}
}
/** merge */
-void StrongSolverTheoryUf::merge( Node a, Node b ){
- RepModel* c = getRepModel( a );
+void StrongSolverTheoryUF::merge( Node a, Node b ){
+ SortModel* c = getSortModel( a );
if( c ){
- Trace("uf-ss-solver") << "StrongSolverTheoryUf: Merge " << a << " " << b << " : " << a.getType() << std::endl;
+ Trace("uf-ss-solver") << "StrongSolverTheoryUF: Merge " << a << " " << b << " : " << a.getType() << std::endl;
c->merge( a, b );
+ }else{
+ if( options::ufssDiseqPropagation() ){
+ d_deq_prop->merge(a, b);
+ }
}
}
/** assert terms are disequal */
-void StrongSolverTheoryUf::assertDisequal( Node a, Node b, Node reason ){
- RepModel* c = getRepModel( a );
+void StrongSolverTheoryUF::assertDisequal( Node a, Node b, Node reason ){
+ SortModel* c = getSortModel( a );
if( c ){
- Trace("uf-ss-solver") << "StrongSolverTheoryUf: Assert disequal " << a << " " << b << " : " << a.getType() << 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 );
+ }else{
+ if( options::ufssDiseqPropagation() ){
+ d_deq_prop->assertDisequal(a, b, reason);
+ }
}
}
/** assert a node */
-void StrongSolverTheoryUf::assertNode( Node n, bool isDecision ){
+void StrongSolverTheoryUF::assertNode( Node n, bool isDecision ){
Trace("uf-ss") << "Assert " << n << " " << isDecision << std::endl;
- if( n.getKind()==CARDINALITY_CONSTRAINT ){
- TypeNode tn = n[0].getType();
- Assert( tn.isSort() );
- Assert( d_rep_model[tn] );
- long nCard = n[1].getConst<Rational>().getNumerator().getLong();
- d_rep_model[tn]->assertCardinality( d_out, nCard, true );
- }else if( n.getKind()==NOT && n[0].getKind()==CARDINALITY_CONSTRAINT ){
- Node nn = n[0];
- TypeNode tn = nn[0].getType();
+ bool polarity = n.getKind() != kind::NOT;
+ TNode lit = polarity ? n : n[0];
+ if( lit.getKind()==CARDINALITY_CONSTRAINT ){
+ TypeNode tn = lit[0].getType();
Assert( tn.isSort() );
Assert( d_rep_model[tn] );
- long nCard = nn[1].getConst<Rational>().getNumerator().getLong();
- d_rep_model[tn]->assertCardinality( d_out, nCard, false );
+ long nCard = lit[1].getConst<Rational>().getNumerator().getLong();
+ d_rep_model[tn]->assertCardinality( d_out, nCard, polarity );
}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, 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();
+ if( Trace.isOn("uf-ss-warn") ){
+ ////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, SortModel* >::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();
+ }
}
}
}
+ if( lit.getKind()!=EQUAL ){
+ //it is a predicate
+ if( options::ufssDiseqPropagation() ){
+ d_deq_prop->assertPredicate(lit, polarity);
+ }
+ }
}
Trace("uf-ss") << "Assert: done " << n << " " << isDecision << std::endl;
}
+bool StrongSolverTheoryUF::areDisequal( Node a, Node b ) {
+ if( a==b ){
+ return false;
+ }else{
+ a = d_th->d_equalityEngine.getRepresentative( a );
+ b = d_th->d_equalityEngine.getRepresentative( b );
+ if( d_th->d_equalityEngine.areDisequal( a, b, false ) ){
+ return true;
+ }else{
+ SortModel* c = getSortModel( a );
+ if( c ){
+ return c->areDisequal( a, b );
+ }else{
+ return false;
+ }
+ }
+ }
+}
/** check */
-void StrongSolverTheoryUf::check( Theory::Effort level ){
+void StrongSolverTheoryUF::check( Theory::Effort level ){
if( !d_conflict ){
- Trace("uf-ss-solver") << "StrongSolverTheoryUf: check " << level << std::endl;
+ Trace("uf-ss-solver") << "StrongSolverTheoryUF: check " << level << std::endl;
if( level==Theory::EFFORT_FULL ){
debugPrint( "uf-ss-debug" );
}
@@ -1391,7 +1461,7 @@ void StrongSolverTheoryUf::check( Theory::Effort level ){
return;
}
}
- for( std::map< TypeNode, RepModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
+ for( std::map< TypeNode, SortModel* >::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;
@@ -1403,20 +1473,20 @@ void StrongSolverTheoryUf::check( Theory::Effort level ){
// 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;
+ Trace("uf-ss-solver") << "Done StrongSolverTheoryUF: check " << level << std::endl;
}
}
/** propagate */
-void StrongSolverTheoryUf::propagate( Theory::Effort level ){
- //for( std::map< TypeNode, RepModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
+void StrongSolverTheoryUF::propagate( Theory::Effort level ){
+ //for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
// it->second->propagate( level, d_out );
//}
}
/** 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 StrongSolverTheoryUF::getNextDecisionRequest(){
+ for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
Node n = it->second->getNextDecisionRequest();
if( !n.isNull() ){
return n;
@@ -1425,15 +1495,15 @@ Node StrongSolverTheoryUf::getNextDecisionRequest(){
return Node::null();
}
-void StrongSolverTheoryUf::preRegisterTerm( TNode n ){
+void StrongSolverTheoryUF::preRegisterTerm( TNode n ){
Trace("uf-ss-register") << "Preregister " << n << "." << std::endl;
//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;
+ SortModel* rm = NULL;
if( tn.isSort() ){
Trace("uf-ss-register") << "Preregister sort " << tn << "." << std::endl;
- rm = new SortRepModel( n, d_th->getSatContext(), d_th );
+ rm = new SortModel( n, d_th->getSatContext(), this );
}else{
/*
if( tn==NodeManager::currentNM()->integerType() || tn==NodeManager::currentNM()->realType() ){
@@ -1459,7 +1529,7 @@ void StrongSolverTheoryUf::preRegisterTerm( TNode n ){
}
}
-void StrongSolverTheoryUf::registerQuantifier( Node f ){
+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++ ){
@@ -1469,9 +1539,9 @@ void StrongSolverTheoryUf::registerQuantifier( Node f ){
}
-StrongSolverTheoryUf::RepModel* StrongSolverTheoryUf::getRepModel( Node n ){
+StrongSolverTheoryUF::SortModel* StrongSolverTheoryUF::getSortModel( Node n ){
TypeNode tn = n.getType();
- std::map< TypeNode, RepModel* >::iterator it = d_rep_model.find( tn );
+ std::map< TypeNode, SortModel* >::iterator it = d_rep_model.find( tn );
//pre-register the type if not done already
if( it==d_rep_model.end() ){
preRegisterTerm( n );
@@ -1489,13 +1559,13 @@ StrongSolverTheoryUf::RepModel* StrongSolverTheoryUf::getRepModel( Node n ){
return NULL;
}
-void StrongSolverTheoryUf::notifyRestart(){
+void StrongSolverTheoryUF::notifyRestart(){
}
/** get cardinality for sort */
-int StrongSolverTheoryUf::getCardinality( Node n ) {
- RepModel* c = getRepModel( n );
+int StrongSolverTheoryUF::getCardinality( Node n ) {
+ SortModel* c = getSortModel( n );
if( c ){
return c->getCardinality();
}else{
@@ -1503,27 +1573,27 @@ int StrongSolverTheoryUf::getCardinality( Node n ) {
}
}
-void StrongSolverTheoryUf::getRepresentatives( Node n, std::vector< Node >& reps ){
- RepModel* c = getRepModel( n );
+void StrongSolverTheoryUF::getRepresentatives( Node n, std::vector< Node >& reps ){
+ SortModel* c = getSortModel( n );
if( c ){
c->getRepresentatives( reps );
}
}
-bool StrongSolverTheoryUf::minimize( TheoryModel* m ){
- for( std::map< TypeNode, RepModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
+bool StrongSolverTheoryUF::minimize( TheoryModel* m ){
+ for( std::map< TypeNode, SortModel* >::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 ){
+ for( std::map< TypeNode, SortModel* >::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;
}
//print debug
-void StrongSolverTheoryUf::debugPrint( const char* c ){
+void StrongSolverTheoryUF::debugPrint( const char* c ){
//EqClassesIterator< TheoryUF::NotifyClass > eqc_iter( &((TheoryUF*)d_th)->d_equalityEngine );
//while( !eqc_iter.isFinished() ){
// Debug( c ) << "Eq class [[" << (*eqc_iter) << "]]" << std::endl;
@@ -1537,28 +1607,28 @@ void StrongSolverTheoryUf::debugPrint( const char* c ){
// eqc_iter++;
//}
- for( std::map< TypeNode, RepModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
+ for( std::map< TypeNode, SortModel* >::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 ){
+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 ){
+ for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
it->second->debugModel( m );
}
}
}
-StrongSolverTheoryUf::Statistics::Statistics():
- d_clique_conflicts("StrongSolverTheoryUf::Clique_Conflicts", 0),
- d_clique_lemmas("StrongSolverTheoryUf::Clique_Lemmas", 0),
- d_split_lemmas("StrongSolverTheoryUf::Split_Lemmas", 0),
- d_disamb_term_lemmas("StrongSolverTheoryUf::Disambiguate_Term_Lemmas", 0),
- d_totality_lemmas("StrongSolverTheoryUf::Totality_Lemmas", 0),
- d_max_model_size("StrongSolverTheoryUf::Max_Model_Size", 1)
+StrongSolverTheoryUF::Statistics::Statistics():
+ d_clique_conflicts("StrongSolverTheoryUF::Clique_Conflicts", 0),
+ d_clique_lemmas("StrongSolverTheoryUF::Clique_Lemmas", 0),
+ d_split_lemmas("StrongSolverTheoryUF::Split_Lemmas", 0),
+ d_disamb_term_lemmas("StrongSolverTheoryUF::Disambiguate_Term_Lemmas", 0),
+ d_totality_lemmas("StrongSolverTheoryUF::Totality_Lemmas", 0),
+ d_max_model_size("StrongSolverTheoryUF::Max_Model_Size", 1)
{
StatisticsRegistry::registerStat(&d_clique_conflicts);
StatisticsRegistry::registerStat(&d_clique_lemmas);
@@ -1568,7 +1638,7 @@ StrongSolverTheoryUf::Statistics::Statistics():
StatisticsRegistry::registerStat(&d_max_model_size);
}
-StrongSolverTheoryUf::Statistics::~Statistics(){
+StrongSolverTheoryUF::Statistics::~Statistics(){
StatisticsRegistry::unregisterStat(&d_clique_conflicts);
StatisticsRegistry::unregisterStat(&d_clique_lemmas);
StatisticsRegistry::unregisterStat(&d_split_lemmas);
@@ -1647,3 +1717,73 @@ bool TermDisambiguator::involvesRelevantType( Node n ){
}
return false;
}
+
+DisequalityPropagator::DisequalityPropagator(QuantifiersEngine* qe, StrongSolverTheoryUF* ufss) :
+ d_qe(qe), d_ufss(ufss){
+ d_true = NodeManager::currentNM()->mkConst( true );
+ d_false = NodeManager::currentNM()->mkConst( false );
+}
+
+void DisequalityPropagator::checkEquivalenceClass( Node t, Node eqc ) {
+ if( t.getKind()==APPLY_UF ){
+ Node op = t.getOperator();
+ eqc = d_ufss->getTheory()->getEqualityEngine()->getRepresentative( eqc );
+ eq::EqClassIterator eqc_i(eqc, d_ufss->getTheory()->getEqualityEngine());
+ while( !eqc_i.isFinished() ){
+ Node s = *eqc_i;
+ if( s.getKind()==APPLY_UF && s.getOperator()==op ){
+ int unkIndex = -1;
+ for( size_t i=0; i<t.getNumChildren(); i++ ){
+ //should consult strong solver since it knows more disequalities
+ if( d_ufss->areDisequal( t[i], s[i] ) ){
+ //if( d_qe->getEqualityQuery()->areDisequal( t[i], s[i] ) ){
+ unkIndex = -1;
+ break;
+ }else if( !d_qe->getEqualityQuery()->areEqual( t[i], s[i] ) ){
+ if( unkIndex==-1 ){
+ unkIndex = i;
+ }else{
+ unkIndex = -1;
+ break;
+ }
+ }
+ }
+ if( unkIndex!=-1 ){
+ Trace("deq-prop") << "propagate disequality " << t[unkIndex] << " " << s[unkIndex] << std::endl;
+ d_ufss->assertDisequal(t[unkIndex], s[unkIndex], Node::null());
+ ++( d_statistics.d_propagations );
+ if( d_ufss->isConflict() ){
+ return;
+ }
+ }
+ }
+ ++eqc_i;
+ }
+ }
+}
+
+/** merge */
+void DisequalityPropagator::merge( Node a, Node b ){
+
+}
+
+/** assert terms are disequal */
+void DisequalityPropagator::assertDisequal( Node a, Node b, Node reason ){
+ Trace("deq-prop") << "Notify disequal : " << a << " " << b << std::endl;
+}
+
+
+void DisequalityPropagator::assertPredicate( Node p, bool polarity ) {
+ Trace("deq-prop") << "Assert predicate : " << p << " " << polarity << std::endl;
+ checkEquivalenceClass( p, polarity ? d_false : d_true );
+}
+
+DisequalityPropagator::Statistics::Statistics():
+ d_propagations("StrongSolverTheoryUF::Disequality_Propagations", 0)
+{
+ StatisticsRegistry::registerStat(& d_propagations);
+}
+
+DisequalityPropagator::Statistics::~Statistics(){
+ StatisticsRegistry::unregisterStat(& d_propagations);
+} \ No newline at end of file
diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h
index ceb59d5c3..33493248d 100644
--- a/src/theory/uf/theory_uf_strong_solver.h
+++ b/src/theory/uf/theory_uf_strong_solver.h
@@ -31,8 +31,9 @@ namespace uf {
class TheoryUF;
class TermDisambiguator;
+class DisequalityPropagator;
-class StrongSolverTheoryUf{
+class StrongSolverTheoryUF{
protected:
typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
@@ -42,51 +43,14 @@ protected:
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 SortRepModel : public RepModel {
+ class SortModel {
public:
/** a partition of the current equality graph for which cliques can occur internally */
class Region {
public:
/** conflict find pointer */
- SortRepModel* d_cf;
+ SortModel* d_cf;
/** information stored about each node in region */
class RegionNodeInfo {
public:
@@ -142,7 +106,7 @@ public:
void setRep( Node n, bool valid );
public:
//constructor
- Region( SortRepModel* cf, context::Context* c ) : d_cf( cf ), d_testCliqueSize( c, 0 ),
+ Region( SortModel* 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 ) {
}
@@ -186,8 +150,10 @@ public:
void debugPrint( const char* c, bool incClique = false );
};
private:
- /** theory uf pointer */
- TheoryUF* d_th;
+ /** the type this model is for */
+ TypeNode d_type;
+ /** strong solver pointer */
+ StrongSolverTheoryUF* d_thss;
/** regions used to d_region_index */
context::CDO< unsigned > d_regions_index;
/** vector of regions */
@@ -256,8 +222,8 @@ public:
/** get totality lemma terms */
Node getTotalityLemmaTerm( int cardinality, int i );
public:
- SortRepModel( Node n, context::Context* c, TheoryUF* th );
- virtual ~SortRepModel(){}
+ SortModel( Node n, context::Context* c, StrongSolverTheoryUF* thss );
+ virtual ~SortModel(){}
/** initialize */
void initialize( OutputChannel* out );
/** new node */
@@ -266,6 +232,8 @@ public:
void merge( Node a, Node b );
/** assert terms are disequal */
void assertDisequal( Node a, Node b, Node reason );
+ /** are disequal */
+ bool areDisequal( Node a, Node b );
/** check */
void check( Theory::Effort level, OutputChannel* out );
/** propagate */
@@ -291,7 +259,7 @@ public:
public:
/** get number of regions (for debugging) */
int getNumRegions();
- }; /** class SortRepModel */
+ }; /** class SortModel */
private:
/** The output channel for the strong solver. */
OutputChannel* d_out;
@@ -300,19 +268,31 @@ private:
/** Are we in conflict */
context::CDO<bool> d_conflict;
/** rep model structure, one for each type */
- std::map< TypeNode, RepModel* > d_rep_model;
+ std::map< TypeNode, SortModel* > d_rep_model;
/** all types */
std::vector< TypeNode > d_conf_types;
/** whether conflict find data structures have been initialized */
TypeNodeBoolMap d_rep_model_init;
/** get conflict find */
- RepModel* getRepModel( Node n );
+ SortModel* getSortModel( Node n );
private:
/** term disambiguator */
TermDisambiguator* d_term_amb;
+ /** disequality propagator */
+ DisequalityPropagator* d_deq_prop;
public:
- StrongSolverTheoryUf(context::Context* c, context::UserContext* u, OutputChannel& out, TheoryUF* th);
- ~StrongSolverTheoryUf() {}
+ StrongSolverTheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, TheoryUF* th);
+ ~StrongSolverTheoryUF() {}
+ /** get theory */
+ TheoryUF* getTheory() { return d_th; }
+ /** term disambiguator */
+ TermDisambiguator* getTermDisambiguator() { return d_term_amb; }
+ /** disequality propagator */
+ DisequalityPropagator* getDisequalityPropagator() { return d_deq_prop; }
+ /** get default sat context */
+ context::Context* getSatContext();
+ /** get default output channel */
+ OutputChannel& getOutputChannel();
/** new node */
void newEqClass( Node n );
/** merge */
@@ -321,6 +301,8 @@ public:
void assertDisequal( Node a, Node b, Node reason );
/** assert node */
void assertNode( Node n, bool isDecision );
+ /** are disequal */
+ bool areDisequal( Node a, Node b );
public:
/** check */
void check( Theory::Effort level );
@@ -336,7 +318,7 @@ public:
void notifyRestart();
public:
/** identify */
- std::string identify() const { return std::string("StrongSolverTheoryUf"); }
+ std::string identify() const { return std::string("StrongSolverTheoryUF"); }
//print debug
void debugPrint( const char* c );
/** debug a model */
@@ -368,7 +350,7 @@ public:
};
/** statistics class */
Statistics d_statistics;
-};/* class StrongSolverTheoryUf */
+};/* class StrongSolverTheoryUF */
class TermDisambiguator
@@ -387,6 +369,37 @@ public:
int disambiguateTerms( OutputChannel* out );
};
+class DisequalityPropagator
+{
+private:
+ /** quantifiers engine */
+ QuantifiersEngine* d_qe;
+ /** strong solver */
+ StrongSolverTheoryUF* d_ufss;
+ /** true,false */
+ Node d_true;
+ Node d_false;
+ /** check term t against equivalence class that t is disequal from */
+ void checkEquivalenceClass( Node t, Node eqc );
+public:
+ DisequalityPropagator(QuantifiersEngine* qe, StrongSolverTheoryUF* ufss);
+ /** merge */
+ void merge( Node a, Node b );
+ /** assert terms are disequal */
+ void assertDisequal( Node a, Node b, Node reason );
+ /** assert predicate */
+ void assertPredicate( Node p, bool polarity );
+public:
+ class Statistics {
+ public:
+ IntStat d_propagations;
+ Statistics();
+ ~Statistics();
+ };
+ /** statistics class */
+ Statistics d_statistics;
+};
+
}
}/* CVC4::theory namespace */
}/* CVC4 namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback