VarNameAttr(), s)) {
out << s;
} else {
- out << "var_" << d_id << "[" << this << "]";
+ out << "var_" << d_id;
}
if(types) {
// print the whole type, but not *its* type
/**
* Is this a predicate type, i.e. if it's a function type mapping to Boolean.
- * Aall predicate types are also function types.
+ * All predicate types are also function types.
* @return true if the type is a predicate type
*/
bool isPredicate() const;
| /* get-assertions */
GET_ASSERTIONS_TOK
{ cmd = new GetAssertionsCommand; }
+ | /* push */
+ PUSH_TOK k=INTEGER_LITERAL
+ { unsigned n = AntlrInput::tokenToUnsigned(k);
+ if(n == 0) {
+ cmd = new EmptyCommand;
+ } else if(n == 1) {
+ cmd = new PushCommand;
+ } else {
+ CommandSequence* seq = new CommandSequence;
+ do {
+ seq->addCommand(new PushCommand);
+ } while(--n > 0);
+ cmd = seq;
+ }
+ }
+ | POP_TOK k=INTEGER_LITERAL
+ { unsigned n = AntlrInput::tokenToUnsigned(k);
+ if(n == 0) {
+ cmd = new EmptyCommand;
+ } else if(n == 1) {
+ cmd = new PopCommand;
+ } else {
+ CommandSequence* seq = new CommandSequence;
+ do {
+ seq->addCommand(new PopCommand);
+ } while(--n > 0);
+ cmd = seq;
+ }
+ }
| EXIT_TOK
{ cmd = NULL; }
;
GET_INFO_TOK : 'get-info';
SET_OPTION_TOK : 'set-option';
GET_OPTION_TOK : 'get-option';
+PUSH_TOK : 'push';
+POP_TOK : 'pop';
// operators (NOTE: theory symbols go here)
AMPERSAND_TOK : '&';
const NodeCache& getNodeCache() const {
return d_nodeCache;
}
-}; /* class CnfStream */
+};/* class CnfStream */
/**
* TseitinCnfStream is based on the following recursive algorithm
return Result(result ? Result::SAT : Result::UNSAT);
}
+Node PropEngine::getValue(TNode node) {
+ Assert(node.getKind() == kind::VARIABLE &&
+ node.getType().isBoolean());
+ SatLiteralValue v = d_satSolver->value(d_cnfStream->getLiteral(node));
+ if(v == l_True) {
+ return NodeManager::currentNM()->mkConst(true);
+ } else if(v == l_False) {
+ return NodeManager::currentNM()->mkConst(false);
+ } else {
+ Assert(v == l_Undef);
+ return Node::null();
+ }
+}
+
void PropEngine::push() {
Assert(!d_inCheckSat, "Sat solver in solve()!");
Debug("prop") << "push()" << endl;
*/
Result checkSat();
+ /**
+ * Get the value of a boolean variable.
+ *
+ * @return mkConst<true>, mkConst<false>, or Node::null() if
+ * unassigned.
+ */
+ Node getValue(TNode node);
+
/**
* Push the context level.
*/
}
#endif /* __CVC4_USE_MINISAT */
-/** Interface encapsulating the "input" to the solver, e.g., from the
- * CNF converter.
- *
+/** Interface encapsulating the "input" to the solver, e.g., from the
+ * CNF converter.
+ *
* TODO: Is it possible to push the typedefs of SatClause and SatVariable
* into here, somehow?
*/
void setCnfStream(CnfStream* cnfStream);
SatLiteralValue value(SatLiteral l);
-};
+};/* class SatSolver */
/* Functions that delegate to the concrete SAT solver. */
d_decisionEngine(NULL),
d_theoryEngine(NULL),
d_propEngine(NULL),
- d_assertionList(NULL) {
+ d_assertionList(NULL),
+ d_haveAdditions(false),
+ d_lastResult() {
NodeManagerScope nms(d_nodeManager);
void SmtEngine::setInfo(const string& key, const SExpr& value)
throw(BadOptionException) {
- if(key == ":status" ||
+ Debug("smt") << "SMT setInfo(" << key << ", " << value << ")" << endl;
+ if(key == ":name" ||
+ key == ":status" ||
key == ":source" ||
key == ":category" ||
key == ":difficulty" ||
const SExpr& SmtEngine::getInfo(const string& key) const
throw(BadOptionException) {
+ Debug("smt") << "SMT getInfo(" << key << ")" << endl;
// FIXME implement me
throw BadOptionException();
}
void SmtEngine::setOption(const string& key, const SExpr& value)
throw(BadOptionException) {
+ Debug("smt") << "SMT setOption(" << key << ", " << value << ")" << endl;
// FIXME implement me
throw BadOptionException();
}
const SExpr& SmtEngine::getOption(const string& key) const
throw(BadOptionException) {
+ Debug("smt") << "SMT getOption(" << key << ")" << endl;
// FIXME implement me
throw BadOptionException();
}
void SmtEngine::defineFunction(Expr func,
const vector<Expr>& formals,
Expr formula) {
+ Debug("smt") << "SMT defineFunction(" << func << ")" << endl;
NodeManagerScope nms(d_nodeManager);
Type formulaType = formula.getType(true);// type check body
if(formulaType != FunctionType(func.getType()).getRangeType()) {
}
TNode formulaNode = formula.getTNode();
DefinedFunction def(funcNode, formalsNodes, formulaNode);
+ d_haveAdditions = true;
d_definedFunctions->insert(funcNode, def);
}
void SmtEnginePrivate::addFormula(SmtEngine& smt, TNode n)
throw(NoSuchFunctionException, AssertionException) {
Debug("smt") << "push_back assertion " << n << endl;
+ smt.d_haveAdditions = true;
smt.d_propEngine->assertFormula(SmtEnginePrivate::preprocess(smt, n));
}
}
Result SmtEngine::checkSat(const BoolExpr& e) {
+ Assert(e.getExprManager() == d_exprManager);
NodeManagerScope nms(d_nodeManager);
Debug("smt") << "SMT checkSat(" << e << ")" << endl;
ensureBoolean(e);// ensure expr is type-checked at this point
SmtEnginePrivate::addFormula(*this, e.getNode());
Result r = check().asSatisfiabilityResult();
+ d_lastResult = r;
+ d_haveAdditions = false;
Debug("smt") << "SMT checkSat(" << e << ") ==> " << r << endl;
return r;
}
Result SmtEngine::query(const BoolExpr& e) {
+ Assert(e.getExprManager() == d_exprManager);
NodeManagerScope nms(d_nodeManager);
Debug("smt") << "SMT query(" << e << ")" << endl;
ensureBoolean(e);// ensure expr is type-checked at this point
SmtEnginePrivate::addFormula(*this, e.getNode().notNode());
Result r = check().asValidityResult();
+ d_lastResult = r;
+ d_haveAdditions = false;
Debug("smt") << "SMT query(" << e << ") ==> " << r << endl;
return r;
}
Result SmtEngine::assertFormula(const BoolExpr& e) {
+ Assert(e.getExprManager() == d_exprManager);
NodeManagerScope nms(d_nodeManager);
Debug("smt") << "SMT assertFormula(" << e << ")" << endl;
ensureBoolean(e);// type check node
+ if(d_assertionList != NULL) {
+ d_assertionList->push_back(e);
+ }
SmtEnginePrivate::addFormula(*this, e.getNode());
return quickCheck().asValidityResult();
}
Expr SmtEngine::simplify(const Expr& e) {
+ Assert(e.getExprManager() == d_exprManager);
NodeManagerScope nms(d_nodeManager);
e.getType(true);// ensure expr is type-checked at this point
Debug("smt") << "SMT simplify(" << e << ")" << endl;
Unimplemented();
}
-Expr SmtEngine::getValue(Expr term)
+Expr SmtEngine::getValue(Expr e)
throw(ModalException, AssertionException) {
+ Assert(e.getExprManager() == d_exprManager);
+ Type type = e.getType(true);// ensure expr is type-checked at this point
+ Debug("smt") << "SMT getValue(" << e << ")" << endl;
if(!d_options->interactive) {
const char* msg =
"Cannot get value when not in interactive mode.";
"Cannot get value when produce-models options is off.";
throw ModalException(msg);
}
- // TODO also check that the last query was sat/unknown, without intervening
- // assertions
+ if(d_lastResult.asSatisfiabilityResult() != Result::SAT ||
+ d_haveAdditions) {
+ const char* msg =
+ "Cannot get value unless immediately proceded by SAT/INVALID response.";
+ throw ModalException(msg);
+ }
+ if(type.isFunction() || type.isPredicate() ||
+ type.isKind() || type.isSortConstructor()) {
+ const char* msg =
+ "Cannot get value of a function, predicate, or sort.";
+ throw ModalException(msg);
+ }
NodeManagerScope nms(d_nodeManager);
- Type type = term.getType(true);// ensure expr is type-checked at this point
- SmtEnginePrivate::preprocess(*this, term.getNode());
+ Node eNode = e.getNode();
+ Node n = SmtEnginePrivate::preprocess(*this, eNode);
- Unimplemented();
+ Debug("smt") << "--- getting value of " << n << endl;
+ Node resultNode = d_theoryEngine->getValue(n);
+
+ // type-check the result we got
+ Assert(resultNode.getType(true) == eNode.getType());
+ return Expr(d_exprManager, new Node(resultNode));
}
SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) {
+ Debug("smt") << "SMT getAssignment()" << endl;
if(!d_options->produceAssignments) {
const char* msg =
"Cannot get the current assignment when produce-assignments option is off.";
Unimplemented();
}
-vector<Expr> SmtEngine::getAssertions() throw(ModalException, AssertionException) {
+vector<Expr> SmtEngine::getAssertions()
+ throw(ModalException, AssertionException) {
+ Debug("smt") << "SMT getAssertions()" << endl;
if(!d_options->interactive) {
const char* msg =
"Cannot query the current assertion list when not in interactive mode.";
void SmtEngine::push() {
NodeManagerScope nms(d_nodeManager);
Debug("smt") << "SMT push()" << endl;
- Unimplemented();
+ d_context->push();
+ d_propEngine->push();
+ Debug("userpushpop") << "SmtEngine: pushed to level "
+ << d_context->getLevel() << endl;
}
void SmtEngine::pop() {
NodeManagerScope nms(d_nodeManager);
Debug("smt") << "SMT pop()" << endl;
- Unimplemented();
+ d_propEngine->pop();
+ d_context->pop();
+ Debug("userpushpop") << "SmtEngine: popped to level "
+ << d_context->getLevel() << endl;
+ // clear out last result: get-value/get-assignment no longer
+ // available here
+ d_lastResult = Result();
}
}/* CVC4 namespace */
*/
AssertionList* d_assertionList;
+ /**
+ * Whether or not we have added any
+ * assertions/declarations/definitions since the last checkSat/query
+ * (and therefore we're not responsible for an assignment).
+ */
+ bool d_haveAdditions;
+
+ /**
+ * Result of last checkSat/query.
+ */
+ Result d_lastResult;
+
/**
* This is called by the destructor, just before destroying the
* PropEngine, TheoryEngine, and DecisionEngine (in that order). It
Expr simplify(const Expr& e);
/**
- * Get the assigned value of a term (only if preceded by a SAT or
- * INVALID query). Only permitted if the SmtEngine is set to
- * operate interactively and produce-models is on.
+ * Get the assigned value of an expr (only if immediately preceded
+ * by a SAT or INVALID query). Only permitted if the SmtEngine is
+ * set to operate interactively and produce-models is on.
*/
- Expr getValue(Expr term) throw(ModalException, AssertionException);
+ Expr getValue(Expr e) throw(ModalException, AssertionException);
/**
- * Get the assigned value of a term (only if preceded by a SAT or
+ * Get the assignment (only if immediately preceded by a SAT or
* INVALID query). Only permitted if the SmtEngine is set to
* operate interactively and produce-assignments is on.
*/
using namespace CVC4;
std::ostream& CVC4::operator<<(std::ostream& os, const DeltaRational& dq){
- return os << "(" << dq.getNoninfintestimalPart()
- << "," << dq.getInfintestimalPart() << ")";
+ return os << "(" << dq.getNoninfinitesimalPart()
+ << "," << dq.getInfinitesimalPart() << ")";
}
std::string DeltaRational::toString() const {
- return "(" + getNoninfintestimalPart().toString() + "," +
- getInfintestimalPart().toString() + ")";
+ return "(" + getNoninfinitesimalPart().toString() + "," +
+ getInfinitesimalPart().toString() + ")";
}
DeltaRational(const CVC4::Rational& base, const CVC4::Rational& coeff) :
c(base), k(coeff) {}
- const CVC4::Rational& getInfintestimalPart() const {
+ const CVC4::Rational& getInfinitesimalPart() const {
return k;
}
- const CVC4::Rational& getNoninfintestimalPart() const {
+ const CVC4::Rational& getNoninfinitesimalPart() const {
return c;
}
Assert(d_coeffs[var_i] != Rational(0,1));
}
}
-void Row::subsitute(Row& row_s){
+void Row::substitute(Row& row_s){
ArithVar x_s = row_s.basicVar();
Assert(has(x_s));
Assert(isActiveBasicVariable(var));
Row* row_var = lookup(var);
- row_current->subsitute(*row_var);
+ row_current->substitute(*row_var);
}
}
}
Row* row_k = lookup(basic);
if(row_k->has(x_s)){
d_activityMonitor.increaseActivity(basic, 30);
- row_k->subsitute(*row_s);
+ row_k->substitute(*row_s);
}
}
}
Row* row_var = isActiveBasicVariable(var) ? lookup(var) : lookupEjected(var);
Assert(row_var != row);
- row->subsitute(*row_var);
+ row->substitute(*row_var);
i = row->begin();
endIter = row->end();
void pivot(ArithVar x_j);
- void subsitute(Row& row_s);
+ void substitute(Row& row_s);
void printRow();
};
#include "expr/metakind.h"
#include "expr/node_builder.h"
+#include "theory/theory_engine.h"
+
#include "util/rational.h"
#include "util/integer.h"
}
}
}
+
+Node TheoryArith::getValue(TNode n, TheoryEngine* engine) {
+ NodeManager* nodeManager = NodeManager::currentNM();
+
+ switch(n.getKind()) {
+ case kind::VARIABLE: {
+ DeltaRational drat = d_partialModel.getAssignment(asArithVar(n));
+ // FIXME our infinitesimal is fixed here at 1e-06
+ return nodeManager->
+ mkConst( drat.getNoninfinitesimalPart() +
+ drat.getInfinitesimalPart() * Rational(1, 1000000) );
+ }
+
+ case kind::EQUAL: // 2 args
+ return nodeManager->
+ mkConst( engine->getValue(n[0]) == engine->getValue(n[1]) );
+
+ case kind::PLUS: { // 2+ args
+ Rational value = d_constants.d_ZERO;
+ for(TNode::iterator i = n.begin(),
+ iend = n.end();
+ i != iend;
+ ++i) {
+ value += engine->getValue(*i).getConst<Rational>();
+ }
+ return nodeManager->mkConst(value);
+ }
+
+ case kind::MULT: { // 2+ args
+ Rational value = d_constants.d_ONE;
+ for(TNode::iterator i = n.begin(),
+ iend = n.end();
+ i != iend;
+ ++i) {
+ value *= engine->getValue(*i).getConst<Rational>();
+ }
+ return nodeManager->mkConst(value);
+ }
+
+ case kind::MINUS: // 2 args
+ // should have been rewritten
+ Unreachable();
+
+ case kind::UMINUS: // 1 arg
+ // should have been rewritten
+ Unreachable();
+
+ case kind::DIVISION: // 2 args
+ return nodeManager->mkConst( engine->getValue(n[0]).getConst<Rational>() /
+ engine->getValue(n[1]).getConst<Rational>() );
+
+ case kind::IDENTITY: // 1 arg
+ return engine->getValue(n[0]);
+
+ case kind::LT: // 2 args
+ return nodeManager->mkConst( engine->getValue(n[0]).getConst<Rational>() <
+ engine->getValue(n[1]).getConst<Rational>() );
+
+ case kind::LEQ: // 2 args
+ return nodeManager->mkConst( engine->getValue(n[0]).getConst<Rational>() <=
+ engine->getValue(n[1]).getConst<Rational>() );
+
+ case kind::GT: // 2 args
+ return nodeManager->mkConst( engine->getValue(n[0]).getConst<Rational>() >
+ engine->getValue(n[1]).getConst<Rational>() );
+
+ case kind::GEQ: // 2 args
+ return nodeManager->mkConst( engine->getValue(n[0]).getConst<Rational>() >=
+ engine->getValue(n[1]).getConst<Rational>() );
+
+ default:
+ Unhandled(n.getKind());
+ }
+}
void propagate(Effort e);
void explain(TNode n, Effort e);
+ Node getValue(TNode n, TheoryEngine* engine);
+
void shutdown(){ }
std::string identify() const { return std::string("TheoryArith"); }
#include "theory/arrays/theory_arrays.h"
+#include "theory/theory_engine.h"
#include "expr/kind.h"
}
Debug("arrays") << "TheoryArrays::check(): done" << endl;
}
+
+Node TheoryArrays::getValue(TNode n, TheoryEngine* engine) {
+ NodeManager* nodeManager = NodeManager::currentNM();
+
+ switch(n.getKind()) {
+
+ case kind::VARIABLE:
+ Unhandled(kind::VARIABLE);
+
+ case kind::EQUAL: // 2 args
+ return nodeManager->
+ mkConst( engine->getValue(n[0]) == engine->getValue(n[1]) );
+
+ default:
+ Unhandled(n.getKind());
+ }
+}
void check(Effort e);
void propagate(Effort e) { }
void explain(TNode n, Effort e) { }
+ Node getValue(TNode n, TheoryEngine* engine);
void shutdown() { }
std::string identify() const { return std::string("TheoryArrays"); }
};/* class TheoryArrays */
#include "theory/theory.h"
#include "theory/booleans/theory_bool.h"
+#include "theory/theory_engine.h"
namespace CVC4 {
namespace theory {
namespace booleans {
-
RewriteResponse TheoryBool::preRewrite(TNode n, bool topLevel) {
if(n.getKind() == kind::IFF) {
NodeManager* nodeManager = NodeManager::currentNM();
return RewriteComplete(n);
}
+Node TheoryBool::getValue(TNode n, TheoryEngine* engine) {
+ NodeManager* nodeManager = NodeManager::currentNM();
+
+ switch(n.getKind()) {
+ case kind::VARIABLE:
+ // case for Boolean vars is implemented in TheoryEngine (since it
+ // appeals to the PropEngine to get the value)
+ Unreachable();
+
+ case kind::EQUAL: // 2 args
+ // should be handled by IFF
+ Unreachable();
+
+ case kind::NOT: // 1 arg
+ return nodeManager->mkConst(! engine->getValue(n[0]).getConst<bool>());
+
+ case kind::AND: { // 2+ args
+ for(TNode::iterator i = n.begin(),
+ iend = n.end();
+ i != iend;
+ ++i) {
+ if(! engine->getValue(*i).getConst<bool>()) {
+ return nodeManager->mkConst(false);
+ }
+ }
+ return nodeManager->mkConst(true);
+ }
+
+ case kind::IFF: // 2 args
+ return nodeManager->mkConst( engine->getValue(n[0]).getConst<bool>() ==
+ engine->getValue(n[1]).getConst<bool>() );
+
+ case kind::IMPLIES: // 2 args
+ return nodeManager->mkConst( (! engine->getValue(n[0]).getConst<bool>()) ||
+ engine->getValue(n[1]).getConst<bool>() );
+
+ case kind::OR: { // 2+ args
+ for(TNode::iterator i = n.begin(),
+ iend = n.end();
+ i != iend;
+ ++i) {
+ if(engine->getValue(*i).getConst<bool>()) {
+ return nodeManager->mkConst(true);
+ }
+ }
+ return nodeManager->mkConst(false);
+ }
+
+ case kind::XOR: // 2 args
+ return nodeManager->mkConst( engine->getValue(n[0]).getConst<bool>() !=
+ engine->getValue(n[1]).getConst<bool>() );
+
+ case kind::ITE: // 3 args
+ // all ITEs should be gone except (bool,bool,bool) ones
+ Assert( n[1].getType() == nodeManager->booleanType() &&
+ n[2].getType() == nodeManager->booleanType() );
+ return nodeManager->mkConst( engine->getValue(n[0]).getConst<bool>() ?
+ engine->getValue(n[1]).getConst<bool>() :
+ engine->getValue(n[2]).getConst<bool>() );
+
+ default:
+ Unhandled(n.getKind());
+ }
+}
}/* CVC4::theory::booleans namespace */
}/* CVC4::theory namespace */
void propagate(Effort e) { Unimplemented(); }
void explain(TNode n, Effort e) { Unimplemented(); }
+ Node getValue(TNode n, TheoryEngine* engine);
+
RewriteResponse preRewrite(TNode n, bool topLevel);
RewriteResponse postRewrite(TNode n, bool topLevel);
**/
#include "theory/builtin/theory_builtin.h"
+#include "theory/theory_engine.h"
#include "expr/kind.h"
using namespace std;
namespace builtin {
Node TheoryBuiltin::blastDistinct(TNode in) {
- Debug("theory-rewrite") << "TheoryBuiltin::blastDistinct: " << in << std::endl;
+ Debug("theory-rewrite") << "TheoryBuiltin::blastDistinct: "
+ << in << std::endl;
Assert(in.getKind() == kind::DISTINCT);
if(in.getNumChildren() == 2) {
// if this is the case exactly 1 != pair will be generated so the
}
}
+Node TheoryBuiltin::getValue(TNode n, TheoryEngine* engine) {
+ switch(n.getKind()) {
+
+ case kind::VARIABLE:
+ // no variables that the builtin theory is responsible for
+ Unreachable();
+
+ case kind::EQUAL: { // 2 args
+ // has to be an EQUAL over tuples, since all others should be
+ // handled elsewhere
+ Assert(n[0].getKind() == kind::TUPLE &&
+ n[1].getKind() == kind::TUPLE);
+ return NodeManager::currentNM()->
+ mkConst( getValue(n[0], engine) == getValue(n[1], engine) );
+ }
+
+ case kind::TUPLE: { // 2+ args
+ NodeBuilder<> nb(kind::TUPLE);
+ for(TNode::iterator i = n.begin(),
+ iend = n.end();
+ i != iend;
+ ++i) {
+ nb << engine->getValue(*i);
+ }
+ return Node(nb);
+ }
+
+ default:
+ // all other "builtins" should have been rewritten away or handled
+ // by theory engine, or handled elsewhere.
+ Unhandled(n.getKind());
+ }
+}
+
}/* CVC4::theory::builtin namespace */
}/* CVC4::theory */
}/* CVC4 namespace */
void check(Effort e) { Unreachable(); }
void propagate(Effort e) { Unreachable(); }
void explain(TNode n, Effort e) { Unreachable(); }
+ Node getValue(TNode n, TheoryEngine* engine);
void shutdown() { }
RewriteResponse preRewrite(TNode n, bool topLevel);
std::string identify() const { return std::string("TheoryBuiltin"); }
** \todo document this file
**/
-#include "theory_bv.h"
-#include "theory_bv_utils.h"
-#include "theory_bv_rewrite_rules.h"
+#include "theory/bv/theory_bv.h"
+#include "theory/bv/theory_bv_utils.h"
+#include "theory/bv/theory_bv_rewrite_rules.h"
+
+#include "theory/theory_engine.h"
using namespace CVC4;
using namespace CVC4::theory;
return true;
}
+Node TheoryBV::getValue(TNode n, TheoryEngine* engine) {
+ NodeManager* nodeManager = NodeManager::currentNM();
+
+ switch(n.getKind()) {
+
+ case kind::VARIABLE:
+ Unhandled(kind::VARIABLE);
+
+ case kind::EQUAL: // 2 args
+ return nodeManager->
+ mkConst( engine->getValue(n[0]) == engine->getValue(n[1]) );
+
+ default:
+ Unhandled(n.getKind());
+ }
+}
void explain(TNode n, Effort e) { }
+ Node getValue(TNode n, TheoryEngine* engine);
+
RewriteResponse postRewrite(TNode n, bool topLevel);
std::string identify() const { return std::string("TheoryBV"); }
// TODO add compiler annotation "constant function" here
static bool minEffortOnly(Effort e) { return e == MIN_EFFORT; }
static bool quickCheckOrMore(Effort e) { return e >= QUICK_CHECK; }
- static bool quickCheckOnly(Effort e) { return e >= QUICK_CHECK && e < STANDARD; }
+ static bool quickCheckOnly(Effort e) { return e >= QUICK_CHECK &&
+ e < STANDARD; }
static bool standardEffortOrMore(Effort e) { return e >= STANDARD; }
- static bool standardEffortOnly(Effort e) { return e >= STANDARD && e < FULL_EFFORT; }
+ static bool standardEffortOnly(Effort e) { return e >= STANDARD &&
+ e < FULL_EFFORT; }
static bool fullEffort(Effort e) { return e >= FULL_EFFORT; }
/**
* (ITE true x y).
*/
virtual RewriteResponse preRewrite(TNode n, bool topLevel) {
- Debug("theory-rewrite") << "no pre-rewriting to perform for " << n << std::endl;
+ Debug("theory-rewrite") << "no pre-rewriting to perform for "
+ << n << std::endl;
return RewriteComplete(n);
}
* memory leakage).
*/
virtual RewriteResponse postRewrite(TNode n, bool topLevel) {
- Debug("theory-rewrite") << "no post-rewriting to perform for " << n << std::endl;
+ Debug("theory-rewrite") << "no post-rewriting to perform for "
+ << n << std::endl;
return RewriteComplete(n);
}
}
/**
- * This method is called to notify a theory that the node n should be considered a "shared term" by this theory
+ * This method is called to notify a theory that the node n should
+ * be considered a "shared term" by this theory
*/
virtual void addSharedTerm(TNode n) { }
/**
- * This method is called by the shared term manager when a shared term lhs
- * which this theory cares about (either because it received a previous
- * addSharedTerm call with lhs or because it received a previous notifyEq call
- * with lhs as the second argument) becomes equal to another shared term rhs.
- * This call also serves as notice to the theory that the shared term manager
- * now considers rhs the representative for this equivalence class of shared
- * terms, so future notifications for this class will be based on rhs not lhs.
+ * This method is called by the shared term manager when a shared
+ * term lhs which this theory cares about (either because it
+ * received a previous addSharedTerm call with lhs or because it
+ * received a previous notifyEq call with lhs as the second
+ * argument) becomes equal to another shared term rhs. This call
+ * also serves as notice to the theory that the shared term manager
+ * now considers rhs the representative for this equivalence class
+ * of shared terms, so future notifications for this class will be
+ * based on rhs not lhs.
*/
virtual void notifyEq(TNode lhs, TNode rhs) { }
*/
virtual void explain(TNode n, Effort level = FULL_EFFORT) = 0;
+ /**
+ * Return the value of a node (typically used after a ). If the
+ * theory supports model generation but has no value for this node,
+ * it should return Node::null(). If the theory doesn't support
+ * model generation at all, or usually would but doesn't in its
+ * current state, it should throw an exception saying so.
+ *
+ * The TheoryEngine is passed in so that you can recursively request
+ * values for the Node's children. This is important because the
+ * TheoryEngine takes care of simple cases (metakind CONSTANT,
+ * Boolean-valued VARIABLES, ...) and can dispatch to other theories
+ * if that's necessary. Only call your own getValue() recursively
+ * if you *know* that you are responsible handle the Node you're
+ * asking for; other theories can use your types, so be careful
+ * here! To be safe, it's best to delegate back to the
+ * TheoryEngine.
+ *
+ * Usually, you need to handle at least the two cases of EQUAL and
+ * VARIABLE---EQUAL in case a value of yours is on the LHS of an
+ * EQUAL, and VARIABLE for variables of your types. You also need
+ * to support any operators that can survive your rewriter. You
+ * don't need to handle constants, as they are handled by the
+ * TheoryEngine.
+ *
+ * There are some gotchas here. The user may be requesting the
+ * value of an expression that wasn't part of the satisfiable
+ * assertion, or has been declared since. If you don't have a value
+ * and suspect this situation is the case, return Node::null()
+ * rather than throwing an exception.
+ */
+ virtual Node getValue(TNode n, TheoryEngine* engine) = 0;
+
/**
* Identify this theory (for debugging, dynamic configuration,
* etc..)
}/* CVC4::theory namespace */
-inline std::ostream& operator<<(std::ostream& out, const CVC4::theory::Theory& theory) {
+inline std::ostream& operator<<(std::ostream& out,
+ const CVC4::theory::Theory& theory) {
return out << theory.identify();
}
return out;
}/* TheoryEngine::rewrite(TNode in) */
+
+Node TheoryEngine::getValue(TNode node) {
+ kind::MetaKind metakind = node.getMetaKind();
+ // special case: prop engine handles boolean vars
+ if(metakind == kind::metakind::VARIABLE && node.getType().isBoolean()) {
+ return d_propEngine->getValue(node);
+ }
+ // special case: value of a constant == itself
+ if(metakind == kind::metakind::CONSTANT) {
+ return node;
+ }
+
+ // otherwise ask the theory-in-charge
+ return theoryOf(node)->getValue(node, this);
+}/* TheoryEngine::getValue(TNode node) */
+
}/* CVC4 namespace */
return d_theoryOut.d_explanationNode;
}
- inline Node getExplanation(TNode node){
+ inline Node getExplanation(TNode node) {
d_theoryOut.d_explanationNode = Node::null();
theory::Theory* theory =
node.getKind() == kind::NOT ? theoryOf(node[0]) : theoryOf(node);
return d_theoryOut.d_explanationNode;
}
+ Node getValue(TNode node);
+
private:
class Statistics {
public:
**/
#include "theory/uf/morgan/theory_uf_morgan.h"
+#include "theory/theory_engine.h"
#include "expr/kind.h"
#include "util/congruence_closure.h"
Debug("uf") << "uf: end propagate(" << level << ")" << std::endl;
}
+Node TheoryUFMorgan::getValue(TNode n, TheoryEngine* engine) {
+ NodeManager* nodeManager = NodeManager::currentNM();
+
+ switch(n.getKind()) {
+
+ case kind::VARIABLE:
+ case kind::APPLY_UF:
+ if(n.getType().isBoolean()) {
+ if(d_cc.areCongruent(d_trueNode, n)) {
+ return nodeManager->mkConst(true);
+ } else if(d_cc.areCongruent(d_trueNode, n)) {
+ return nodeManager->mkConst(false);
+ }
+ return Node::null();
+ }
+ return d_cc.normalize(n);
+
+ case kind::EQUAL: // 2 args
+ return nodeManager->
+ mkConst( engine->getValue(n[0]) == engine->getValue(n[1]) );
+
+ default:
+ Unhandled(n.getKind());
+ }
+}
+
void TheoryUFMorgan::dump() {
if(!Debug.isOn("uf")) {
return;
void propagate(Effort level);
/**
- * Explains a previously reported conflict. Currently does nothing.
+ * Explains a previously theory-propagated literal.
*
* Overloads void explain(TNode n, Effort level); from theory.h.
* See theory/theory.h for more information about this method.
*/
void explain(TNode n, Effort level) {}
+ /**
+ * Gets a theory value.
+ *
+ * Overloads Node getValue(TNode n); from theory.h.
+ * See theory/theory.h for more information about this method.
+ */
+ Node getValue(TNode n, TheoryEngine* engine);
+
std::string identify() const { return std::string("TheoryUFMorgan"); }
private:
*/
void explain(TNode n, Effort level) {}
+ /**
+ * Get a theory value.
+ *
+ * Overloads Node getValue(TNode n); from theory.h.
+ * See theory/theory.h for more information about this method.
+ */
+ Node getValue(TNode n, TheoryEngine* engine) {
+ Unimplemented("TheoryUFTim doesn't support model generation");
+ }
+
std::string identify() const { return std::string("TheoryUFTim"); }
private:
return explain(eq[0], eq[1]);
}
+ /**
+ * Normalization.
+ */
+ Node normalize(TNode t) const throw(AssertionException);
+
private:
friend std::ostream& operator<< <>(std::ostream& out,
void merge(TNode ec1, TNode ec2);
void mergeProof(TNode a, TNode b, TNode e);
- /**
- * Internal normalization.
- */
- Node normalize(TNode t) const throw(AssertionException);
-
};/* class CongruenceClosure */
}
enum UnknownExplanation whyUnknown();
+ inline bool operator==(Result r) {
+ if(d_which != r.d_which) {
+ return false;
+ }
+ if(d_which == TYPE_SAT) {
+ return d_sat == r.d_sat;
+ }
+ if(d_which == TYPE_VALIDITY) {
+ return d_validity == r.d_validity;
+ }
+ return false;
+ }
+ inline bool operator!=(Result r) {
+ return !(*this == r);
+ }
inline Result asSatisfiabilityResult() const;
inline Result asValidityResult() const;
projects / cvc5.git / commitdiff