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.cpp78
-rw-r--r--src/theory/uf/equality_engine.h4
-rw-r--r--src/theory/uf/kinds3
-rw-r--r--src/theory/uf/symmetry_breaker.cpp51
-rw-r--r--src/theory/uf/symmetry_breaker.h51
-rw-r--r--src/theory/uf/theory_uf.cpp52
-rw-r--r--src/theory/uf/theory_uf.h10
-rw-r--r--src/theory/uf/theory_uf_type_rules.h8
8 files changed, 174 insertions, 83 deletions
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 828d53144..8df323992 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -314,10 +314,10 @@ void EqualityEngine::addTermInternal(TNode t, bool isOperator) {
// How many children are not constants yet
d_subtermsToEvaluate[result] = t.getNumChildren();
for (unsigned i = 0; i < t.getNumChildren(); ++ i) {
- if (isConstant(getNodeId(t[i]))) {
- Debug("equality::evaluation") << d_name << "::eq::addTermInternal(" << t << "): evaluates " << t[i] << std::endl;
- subtermEvaluates(result);
- }
+ if (isConstant(getNodeId(t[i]))) {
+ Debug("equality::evaluation") << d_name << "::eq::addTermInternal(" << t << "): evaluates " << t[i] << std::endl;
+ subtermEvaluates(result);
+ }
}
}
} else {
@@ -335,7 +335,7 @@ void EqualityEngine::addTermInternal(TNode t, bool isOperator) {
} else if (d_constantsAreTriggers && d_isConstant[result]) {
// Non-Boolean constants are trigger terms for all tags
EqualityNodeId tId = getNodeId(t);
- // Setup the new set
+ // Setup the new set
Theory::Set newSetTags = 0;
EqualityNodeId newSetTriggers[THEORY_LAST];
unsigned newSetTriggersSize = THEORY_LAST;
@@ -629,12 +629,12 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
Debug("equality") << d_name << "::eq::merge(" << class1.getFind() << "," << class2.getFind() << "): " << d_nodes[currentId] << " in " << d_nodes[funId] << std::endl;
const FunctionApplication& fun = d_applications[useNode.getApplicationId()].normalized;
// If it's interpreted and we can interpret
- if (fun.isInterpreted() && class1isConstant && !d_isInternal[currentId]) {
- // Get the actual term id
- TNode term = d_nodes[funId];
- subtermEvaluates(getNodeId(term));
- }
- // Check if there is an application with find arguments
+ if (fun.isInterpreted() && class1isConstant && !d_isInternal[currentId]) {
+ // Get the actual term id
+ TNode term = d_nodes[funId];
+ subtermEvaluates(getNodeId(term));
+ }
+ // Check if there is an application with find arguments
EqualityNodeId aNormalized = getEqualityNode(fun.a).getFind();
EqualityNodeId bNormalized = getEqualityNode(fun.b).getFind();
FunctionApplication funNormalized(fun.type, aNormalized, bNormalized);
@@ -972,7 +972,7 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
// If the nodes are the same, we're done
if (t1Id == t2Id){
if( eqp ) {
- eqp->d_node = d_nodes[t1Id];
+ eqp->d_node = ProofManager::currentPM()->mkOp(d_nodes[t1Id]);
}
return;
}
@@ -1029,6 +1029,7 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
MergeReasonType reasonType = d_equalityEdges[currentEdge].getReasonType();
Debug("equality") << d_name << "::eq::getExplanation(): currentEdge = " << currentEdge << ", currentNode = " << currentNode << std::endl;
+ Debug("equality") << d_name << " in currentEdge = (" << d_nodes[currentNode] << "," << d_nodes[edge.getNodeId()] << ")" << std::endl;
EqProof * eqpc = NULL;
//make child proof if a proof is being constructed
@@ -1051,6 +1052,20 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
if( eqpc ){
eqpc->d_children.push_back( eqpc1 );
eqpc->d_children.push_back( eqpc2 );
+ Debug("equality-pf") << "Congruence : " << d_nodes[currentNode] << " " << d_nodes[edgeNode] << std::endl;
+ if( d_nodes[currentNode].getKind()==kind::EQUAL ){
+ //leave node null for now
+ eqpc->d_node = Node::null();
+ }else{
+ Debug("equality-pf") << d_nodes[f1.a] << " / " << d_nodes[f2.a] << ", " << d_nodes[f1.b] << " / " << d_nodes[f2.b] << std::endl;
+ if(d_nodes[f1.a].getKind() == kind::APPLY_UF ||
+ d_nodes[f1.a].getKind() == kind::SELECT ||
+ d_nodes[f1.a].getKind() == kind::STORE) {
+ eqpc->d_node = d_nodes[f1.a];
+ } else {
+ eqpc->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_APPLY_UF, ProofManager::currentPM()->mkOp(d_nodes[f1.a]), d_nodes[f1.b]);
+ }
+ }
}
Debug("equality") << pop;
break;
@@ -1103,13 +1118,14 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
// Construct the equality
Debug("equality") << d_name << "::eq::getExplanation(): adding: " << d_equalityEdges[currentEdge].getReason() << std::endl;
if( eqpc ){
- if( reasonType==MERGED_THROUGH_EQUALITY ){
+ if(reasonType == MERGED_THROUGH_EQUALITY) {
eqpc->d_node = d_equalityEdges[currentEdge].getReason();
- }else{
- //theory-specific proof rule : TODO
- eqpc->d_id = reasonType;
- //eqpc->d_node = d_equalityEdges[currentEdge].getNodeId();
+ } else {
+ // theory-specific proof rule
+ eqpc->d_node = d_nodes[d_equalityEdges[currentEdge].getNodeId()].eqNode(d_nodes[currentNode]);
+ Debug("equality-pf") << "theory eq : " << eqpc->d_node << std::endl;
}
+ eqpc->d_id = reasonType;
}
equalities.push_back(d_equalityEdges[currentEdge].getReason());
break;
@@ -1120,13 +1136,32 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
currentEdge = bfsQueue[currentIndex].edgeId;
currentIndex = bfsQueue[currentIndex].previousIndex;
+ //---from Morgan---
+ if(eqpc != NULL && eqpc->d_id == MERGED_THROUGH_REFLEXIVITY) {
+ if(eqpc->d_node.isNull()) {
+ Assert(eqpc->d_children.size() == 1);
+ EqProof *p = eqpc;
+ eqpc = p->d_children[0];
+ delete p;
+ } else {
+ Assert(eqpc->d_children.empty());
+ }
+ }
+ //---end from Morgan---
+
eqp_trans.push_back( eqpc );
} while (currentEdge != null_id);
- if( eqp ){
- eqp->d_id = MERGED_THROUGH_TRANS;
- eqp->d_children.insert( eqp->d_children.end(), eqp_trans.begin(), eqp_trans.end() );
+ if(eqp) {
+ if(eqp_trans.size() == 1) {
+ *eqp = *eqp_trans[0];
+ delete eqp_trans[0];
+ } else {
+ eqp->d_id = MERGED_THROUGH_TRANS;
+ eqp->d_children.insert( eqp->d_children.end(), eqp_trans.begin(), eqp_trans.end() );
+ eqp->d_node = NodeManager::currentNM()->mkNode(d_nodes[t1Id].getType().isBoolean() ? kind::IFF : kind::EQUAL, d_nodes[t1Id], d_nodes[t2Id]);
+ }
}
// Done
@@ -2057,8 +2092,7 @@ bool EqClassIterator::isFinished() const {
return d_current == null_id;
}
-
-void EqProof::debug_print( const char * c, unsigned tb ){
+void EqProof::debug_print( const char * c, unsigned tb ) const{
for( unsigned i=0; i<tb; i++ ) { Debug( c ) << " "; }
Debug( c ) << d_id << "(";
if( !d_children.empty() || !d_node.isNull() ){
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 87074aebc..9cfa16adf 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -879,8 +879,8 @@ public:
MergeReasonType d_id;
Node d_node;
std::vector< EqProof * > d_children;
- void debug_print( const char * c, unsigned tb = 0 );
-};
+ void debug_print( const char * c, unsigned tb = 0 ) const;
+};/* class EqProof */
} // Namespace eq
} // Namespace theory
diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds
index f0b50b778..888fa140f 100644
--- a/src/theory/uf/kinds
+++ b/src/theory/uf/kinds
@@ -21,6 +21,9 @@ typerule CARDINALITY_CONSTRAINT ::CVC4::theory::uf::CardinalityConstraintTypeRul
operator COMBINED_CARDINALITY_CONSTRAINT 1 "combined cardinality constraint; parameter is a positive integer constant k that bounds the sum of the cardinalities of all sorts in the signature"
typerule COMBINED_CARDINALITY_CONSTRAINT ::CVC4::theory::uf::CombinedCardinalityConstraintTypeRule
+parameterized PARTIAL_APPLY_UF APPLY_UF 1: "partial uninterpreted function application"
+typerule PARTIAL_APPLY_UF ::CVC4::theory::uf::PartialTypeRule
+
operator CARDINALITY_VALUE 1 "cardinality value of sort S: first parameter is (any) term of sort S"
typerule CARDINALITY_VALUE ::CVC4::theory::uf::CardinalityValueTypeRule
diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp
index d5e18ed14..4f7a2667c 100644
--- a/src/theory/uf/symmetry_breaker.cpp
+++ b/src/theory/uf/symmetry_breaker.cpp
@@ -167,7 +167,8 @@ void SymmetryBreaker::Template::reset() {
d_reps.clear();
}
-SymmetryBreaker::SymmetryBreaker(context::Context* context) :
+SymmetryBreaker::SymmetryBreaker(context::Context* context,
+ std::string name) :
ContextNotifyObj(context),
d_assertionsToRerun(context),
d_rerunningAssertions(false),
@@ -178,7 +179,10 @@ SymmetryBreaker::SymmetryBreaker(context::Context* context) :
d_template(),
d_normalizationCache(),
d_termEqs(),
- d_termEqsOnly() {
+ d_termEqsOnly(),
+ d_name(name),
+ d_stats(d_name)
+{
}
class SBGuard {
@@ -461,7 +465,7 @@ void SymmetryBreaker::apply(std::vector<Node>& newClauses) {
Debug("ufsymm") << "UFSYMM =====================================================" << endl
<< "UFSYMM have " << d_permutations.size() << " permutation sets" << endl;
if(!d_permutations.empty()) {
- { TimerStat::CodeTimer codeTimer(d_initNormalizationTimer);
+ { TimerStat::CodeTimer codeTimer(d_stats.d_initNormalizationTimer);
// normalize d_phi
for(vector<Node>::iterator i = d_phi.begin(); i != d_phi.end(); ++i) {
@@ -476,12 +480,12 @@ void SymmetryBreaker::apply(std::vector<Node>& newClauses) {
for(Permutations::iterator i = d_permutations.begin();
i != d_permutations.end();
++i) {
- ++d_permutationSetsConsidered;
+ ++(d_stats.d_permutationSetsConsidered);
const Permutation& p = *i;
Debug("ufsymm") << "UFSYMM looking at permutation: " << p << endl;
size_t n = p.size() - 1;
if(invariantByPermutations(p)) {
- ++d_permutationSetsInvariant;
+ ++(d_stats.d_permutationSetsInvariant);
selectTerms(p);
set<Node> cts;
while(!d_terms.empty() && cts.size() <= n) {
@@ -539,11 +543,11 @@ void SymmetryBreaker::apply(std::vector<Node>& newClauses) {
Node d;
if(disj.getNumChildren() > 1) {
d = disj;
- ++d_clauses;
+ ++(d_stats.d_clauses);
} else {
d = disj[0];
disj.clear();
- ++d_units;
+ ++(d_stats.d_units);
}
if(Debug.isOn("ufsymm")) {
Debug("ufsymm") << "UFSYMM symmetry-breaking clause: " << d << endl;
@@ -569,7 +573,7 @@ void SymmetryBreaker::guessPermutations() {
}
bool SymmetryBreaker::invariantByPermutations(const Permutation& p) {
- TimerStat::CodeTimer codeTimer(d_invariantByPermutationsTimer);
+ TimerStat::CodeTimer codeTimer(d_stats.d_invariantByPermutationsTimer);
// use d_phi
Debug("ufsymm") << "UFSYMM invariantByPermutations()? " << p << endl;
@@ -681,7 +685,7 @@ static bool isSubset(const T1& s, const T2& t) {
}
void SymmetryBreaker::selectTerms(const Permutation& p) {
- TimerStat::CodeTimer codeTimer(d_selectTermsTimer);
+ TimerStat::CodeTimer codeTimer(d_stats.d_selectTermsTimer);
// use d_phi, put into d_terms
Debug("ufsymm") << "UFSYMM selectTerms(): " << p << endl;
@@ -733,6 +737,35 @@ void SymmetryBreaker::selectTerms(const Permutation& p) {
}
}
+SymmetryBreaker::Statistics::Statistics(std::string name)
+ : d_clauses(name + "theory::uf::symmetry_breaker::clauses", 0)
+ , d_units(name + "theory::uf::symmetry_breaker::units", 0)
+ , d_permutationSetsConsidered(name + "theory::uf::symmetry_breaker::permutationSetsConsidered", 0)
+ , d_permutationSetsInvariant(name + "theory::uf::symmetry_breaker::permutationSetsInvariant", 0)
+ , d_invariantByPermutationsTimer(name + "theory::uf::symmetry_breaker::timers::invariantByPermutations")
+ , d_selectTermsTimer(name + "theory::uf::symmetry_breaker::timers::selectTerms")
+ , d_initNormalizationTimer(name + "theory::uf::symmetry_breaker::timers::initNormalization")
+{
+ smtStatisticsRegistry()->registerStat(&d_clauses);
+ smtStatisticsRegistry()->registerStat(&d_units);
+ smtStatisticsRegistry()->registerStat(&d_permutationSetsConsidered);
+ smtStatisticsRegistry()->registerStat(&d_permutationSetsInvariant);
+ smtStatisticsRegistry()->registerStat(&d_invariantByPermutationsTimer);
+ smtStatisticsRegistry()->registerStat(&d_selectTermsTimer);
+ smtStatisticsRegistry()->registerStat(&d_initNormalizationTimer);
+}
+
+SymmetryBreaker::Statistics::~Statistics()
+{
+ smtStatisticsRegistry()->unregisterStat(&d_clauses);
+ smtStatisticsRegistry()->unregisterStat(&d_units);
+ smtStatisticsRegistry()->unregisterStat(&d_permutationSetsConsidered);
+ smtStatisticsRegistry()->unregisterStat(&d_permutationSetsInvariant);
+ smtStatisticsRegistry()->unregisterStat(&d_invariantByPermutationsTimer);
+ smtStatisticsRegistry()->unregisterStat(&d_selectTermsTimer);
+ smtStatisticsRegistry()->unregisterStat(&d_initNormalizationTimer);
+}
+
SymmetryBreaker::Terms::iterator
SymmetryBreaker::selectMostPromisingTerm(Terms& terms) {
// use d_phi
diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h
index 763ced650..5523c1c0d 100644
--- a/src/theory/uf/symmetry_breaker.h
+++ b/src/theory/uf/symmetry_breaker.h
@@ -128,35 +128,30 @@ private:
Node normInternal(TNode phi, size_t level);
Node norm(TNode n);
+ std::string d_name;
+
// === STATISTICS ===
/** number of new clauses that come from the SymmetryBreaker */
- KEEP_STATISTIC(IntStat,
- d_clauses,
- "theory::uf::symmetry_breaker::clauses", 0);
- /** number of new clauses that come from the SymmetryBreaker */
- KEEP_STATISTIC(IntStat,
- d_units,
- "theory::uf::symmetry_breaker::units", 0);
- /** number of potential permutation sets we found */
- KEEP_STATISTIC(IntStat,
- d_permutationSetsConsidered,
- "theory::uf::symmetry_breaker::permutationSetsConsidered", 0);
- /** number of invariant permutation sets we found */
- KEEP_STATISTIC(IntStat,
- d_permutationSetsInvariant,
- "theory::uf::symmetry_breaker::permutationSetsInvariant", 0);
- /** time spent in invariantByPermutations() */
- KEEP_STATISTIC(TimerStat,
- d_invariantByPermutationsTimer,
- "theory::uf::symmetry_breaker::timers::invariantByPermutations");
- /** time spent in selectTerms() */
- KEEP_STATISTIC(TimerStat,
- d_selectTermsTimer,
- "theory::uf::symmetry_breaker::timers::selectTerms");
- /** time spent in initial round of normalization */
- KEEP_STATISTIC(TimerStat,
- d_initNormalizationTimer,
- "theory::uf::symmetry_breaker::timers::initNormalization");
+ struct Statistics {
+ /** number of new clauses that come from the SymmetryBreaker */
+ IntStat d_clauses;
+ IntStat d_units;
+ /** number of potential permutation sets we found */
+ IntStat d_permutationSetsConsidered;
+ /** number of invariant permutation sets we found */
+ IntStat d_permutationSetsInvariant;
+ /** time spent in invariantByPermutations() */
+ TimerStat d_invariantByPermutationsTimer;
+ /** time spent in selectTerms() */
+ TimerStat d_selectTermsTimer;
+ /** time spent in initial round of normalization */
+ TimerStat d_initNormalizationTimer;
+
+ Statistics(std::string name);
+ ~Statistics();
+ };
+
+ Statistics d_stats;
protected:
@@ -167,7 +162,7 @@ protected:
public:
- SymmetryBreaker(context::Context* context);
+ SymmetryBreaker(context::Context* context, std::string name = "");
~SymmetryBreaker() throw() {}
void assertFormula(TNode phi);
void apply(std::vector<Node>& newClauses);
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index e21b7ef7d..93a920f82 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -20,30 +20,34 @@
#include "options/quantifiers_options.h"
#include "options/smt_options.h"
#include "options/uf_options.h"
+#include "proof/proof_manager.h"
+#include "proof/theory_proof.h"
+#include "proof/uf_proof.h"
#include "theory/theory_model.h"
#include "theory/type_enumerator.h"
#include "theory/uf/theory_uf_strong_solver.h"
using namespace std;
-using namespace CVC4;
-using namespace CVC4::theory;
-using namespace CVC4::theory::uf;
+
+namespace CVC4 {
+namespace theory {
+namespace uf {
/** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
TheoryUF::TheoryUF(context::Context* c, context::UserContext* u,
OutputChannel& out, Valuation valuation,
- const LogicInfo& logicInfo, SmtGlobals* globals)
- : Theory(THEORY_UF, c, u, out, valuation, logicInfo, globals),
+ const LogicInfo& logicInfo, SmtGlobals* globals, std::string name)
+ : Theory(THEORY_UF, c, u, out, valuation, logicInfo, globals, name),
d_notify(*this),
/* The strong theory solver can be notified by EqualityEngine::init(),
* so make sure it's initialized first. */
d_thss(NULL),
- d_equalityEngine(d_notify, c, "theory::uf::TheoryUF", true),
+ d_equalityEngine(d_notify, c, name + "theory::uf::TheoryUF", true),
d_conflict(c, false),
d_literalsToPropagate(c),
d_literalsToPropagateIndex(c, 0),
d_functionsTerms(c),
- d_symb(u)
+ d_symb(u, name)
{
// The kinds we are treating as function application in congruence
d_equalityEngine.addFunctionKind(kind::APPLY_UF);
@@ -204,27 +208,29 @@ Node TheoryUF::getNextDecisionRequest(){
}
}
-void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions) {
+void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions, eq::EqProof* pf) {
// Do the work
bool polarity = literal.getKind() != kind::NOT;
TNode atom = polarity ? literal : literal[0];
- eq::EqProof * eqp = d_proofEnabled ? new eq::EqProof : NULL;
if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
- d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions, eqp);
+ d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions, pf);
} else {
- d_equalityEngine.explainPredicate(atom, polarity, assumptions, eqp);
+ d_equalityEngine.explainPredicate(atom, polarity, assumptions, pf);
}
- //for now, just print debug
- //TODO : send the proof outwards : d_out->conflict( lem, eqp );
- if( eqp ){
- eqp->debug_print("uf-pf");
+ if( pf ){
+ Debug("uf-pf") << std::endl;
+ pf->debug_print("uf-pf");
}
}
Node TheoryUF::explain(TNode literal) {
+ return explain(literal, NULL);
+}
+
+Node TheoryUF::explain(TNode literal, eq::EqProof* pf) {
Debug("uf") << "TheoryUF::explain(" << literal << ")" << std::endl;
std::vector<TNode> assumptions;
- explain(literal, assumptions);
+ explain(literal, assumptions, pf);
return mkAnd(assumptions);
}
@@ -508,13 +514,14 @@ void TheoryUF::computeCareGraph() {
}/* TheoryUF::computeCareGraph() */
void TheoryUF::conflict(TNode a, TNode b) {
- //TODO: create EqProof at this level if d_proofEnabled = true
+ eq::EqProof* pf = d_proofsEnabled ? new eq::EqProof() : NULL;
if (a.getKind() == kind::CONST_BOOLEAN) {
- d_conflictNode = explain(a.iffNode(b));
+ d_conflictNode = explain(a.iffNode(b),pf);
} else {
- d_conflictNode = explain(a.eqNode(b));
+ d_conflictNode = explain(a.eqNode(b),pf);
}
- d_out->conflict(d_conflictNode);
+ ProofUF * puf = d_proofsEnabled ? new ProofUF( pf ) : NULL;
+ d_out->conflict(d_conflictNode, puf);
d_conflict = true;
}
@@ -541,3 +548,8 @@ void TheoryUF::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
d_thss->assertDisequal(t1, t2, reason);
}
}
+
+
+} /* namespace CVC4::theory::uf */
+} /* namespace CVC4::theory */
+} /* namespace CVC4 */
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index aff78f53d..bd0016be7 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -128,9 +128,15 @@ private:
/**
* Explain why this literal is true by adding assumptions
+ * with proof (if "pf" is non-NULL).
*/
- void explain(TNode literal, std::vector<TNode>& assumptions);
+ void explain(TNode literal, std::vector<TNode>& assumptions, eq::EqProof* pf);
+ /**
+ * Explain a literal, with proof (if "pf" is non-NULL).
+ */
+ Node explain(TNode literal, eq::EqProof* pf);
+
/** Literals to propagate */
context::CDList<Node> d_literalsToPropagate;
@@ -163,7 +169,7 @@ public:
/** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out,
Valuation valuation, const LogicInfo& logicInfo,
- SmtGlobals* globals);
+ SmtGlobals* globals, std::string name = "");
~TheoryUF();
diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h
index 6faab8517..05b95e9e1 100644
--- a/src/theory/uf/theory_uf_type_rules.h
+++ b/src/theory/uf/theory_uf_type_rules.h
@@ -107,6 +107,14 @@ public:
}
};/* class CardinalityConstraintTypeRule */
+class PartialTypeRule {
+public:
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
+ return n.getOperator().getType().getRangeType();
+ }
+};/* class PartialTypeRule */
+
class CardinalityValueTypeRule {
public:
inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback