In the process of doing this I may have fixed some bugs or some potential bugs so there
may be some user visible results of this refactoring.
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
smt/boolean_terms.h \
smt/boolean_terms.cpp \
smt/logic_exception.h \
+ smt/logic_request.h \
smt/simplification_mode.h \
smt/simplification_mode.cpp \
smt/options_handlers.h \
--- /dev/null
+/********************* */
+/*! \file logic_request.h
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief An object to request logic widening in the running SmtEngine
+ **
+ ** An object to request logic widening in the running SmtEngine. This
+ ** class exists as a proxy between theory code and the SmtEngine, allowing
+ ** a theory to enable another theory in the SmtEngine after initialization
+ ** (thus the usual, public setLogic() cannot be used). This is mainly to
+ ** support features like uninterpreted divide-by-zero (to support the
+ ** partial function DIVISION), where during theory expansion, the theory
+ ** of uninterpreted functions needs to be added to the logic to support
+ ** partial functions.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__LOGIC_REQUEST_H
+#define __CVC4__LOGIC_REQUEST_H
+
+#include "expr/kind.h"
+#include "smt/smt_engine.h"
+
+namespace CVC4 {
+
+class LogicRequest {
+ /** The SmtEngine at play. */
+ SmtEngine& d_smt;
+
+public:
+ LogicRequest(SmtEngine& smt) : d_smt(smt) { }
+
+ /** Widen the logic to include the given theory. */
+ void widenLogic(theory::TheoryId id) {
+ d_smt.d_logic.getUnlockedCopy();
+ d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
+ d_smt.d_logic.enableTheory(id);
+ d_smt.d_logic.lock();
+ }
+
+};/* class LogicRequest */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__LOGIC_REQUEST_H */
#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
#include "smt/model_postprocessor.h"
+#include "smt/logic_request.h"
#include "theory/theory_engine.h"
#include "theory/bv/theory_bv_rewriter.h"
#include "proof/proof_manager.h"
*/
hash_map<Node, Node, NodeHashFunction> d_abstractValues;
- /**
- * Function symbol used to implement uninterpreted undefined string
- * semantics. Needed to deal with partial charat/substr function.
- */
- Node d_ufSubstr;
-
- /**
- * Function symbol used to implement uninterpreted undefined string
- * semantics. Needed to deal with partial str2int function.
- */
- Node d_ufS2I;
-
- /**
- * Function symbol used to implement uninterpreted division-by-zero
- * semantics. Needed to deal with partial division function ("/").
- */
- Node d_divByZero;
-
- /**
- * Maps from bit-vector width to divison-by-zero uninterpreted
- * function symbols.
- */
- hash_map<unsigned, Node> d_BVDivByZero;
- hash_map<unsigned, Node> d_BVRemByZero;
-
- /**
- * Function symbol used to implement uninterpreted
- * int-division-by-zero semantics. Needed to deal with partial
- * function "div".
- */
- Node d_intDivByZero;
-
- /**
- * Function symbol used to implement uninterpreted mod-zero
- * semantics. Needed to deal with partial function "mod".
- */
- Node d_modZero;
-
/** Number of calls of simplify assertions active.
*/
unsigned d_simplifyAssertionsDepth;
d_fakeContext(),
d_abstractValueMap(&d_fakeContext),
d_abstractValues(),
- d_divByZero(),
- d_intDivByZero(),
- d_modZero(),
d_simplifyAssertionsDepth(0),
d_iteSkolemMap(),
d_iteRemover(smt.d_userContext),
void addFormula(TNode n)
throw(TypeCheckingException, LogicException);
- /**
- * Return the uinterpreted function symbol corresponding to division-by-zero
- * for this particular bit-width
- * @param k should be UREM or UDIV
- * @param width
- *
- * @return
- */
- Node getBVDivByZero(Kind k, unsigned width);
-
- /**
- * Returns the node modeling the division-by-zero semantics of node n.
- *
- * @param n
- *
- * @return
- */
- Node expandBVDivByZero(TNode n);
-
/**
* Expand definitions in n.
*/
options::fmfBoundInt.set( true );
Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl;
}
- /*
+ /*
if(! options::rewriteDivk.wasSetByUser()) {
options::rewriteDivk.set( true );
Trace("smt") << "turning on rewrite-divk, for strings-exp" << std::endl;
}
-Node SmtEnginePrivate::getBVDivByZero(Kind k, unsigned width) {
- NodeManager* nm = d_smt.d_nodeManager;
- if (k == kind::BITVECTOR_UDIV) {
- if (d_BVDivByZero.find(width) == d_BVDivByZero.end()) {
- // lazily create the function symbols
- ostringstream os;
- os << "BVUDivByZero_" << width;
- Node divByZero = nm->mkSkolem(os.str(),
- nm->mkFunctionType(nm->mkBitVectorType(width), nm->mkBitVectorType(width)),
- "partial bvudiv", NodeManager::SKOLEM_EXACT_NAME);
- d_BVDivByZero[width] = divByZero;
- }
- return d_BVDivByZero[width];
- }
- else if (k == kind::BITVECTOR_UREM) {
- if (d_BVRemByZero.find(width) == d_BVRemByZero.end()) {
- ostringstream os;
- os << "BVURemByZero_" << width;
- Node divByZero = nm->mkSkolem(os.str(),
- nm->mkFunctionType(nm->mkBitVectorType(width), nm->mkBitVectorType(width)),
- "partial bvurem", NodeManager::SKOLEM_EXACT_NAME);
- d_BVRemByZero[width] = divByZero;
- }
- return d_BVRemByZero[width];
- }
-
- Unreachable();
-}
-
-
-Node SmtEnginePrivate::expandBVDivByZero(TNode n) {
- // we only deal wioth the unsigned division operators as the signed ones should have been
- // expanded in terms of the unsigned operators
- NodeManager* nm = d_smt.d_nodeManager;
- unsigned width = n.getType().getBitVectorSize();
- Node divByZero = getBVDivByZero(n.getKind(), width);
- TNode num = n[0], den = n[1];
- Node den_eq_0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(BitVector(width, Integer(0))));
- Node divByZeroNum = nm->mkNode(kind::APPLY_UF, divByZero, num);
- Node divTotalNumDen = nm->mkNode(n.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_UDIV_TOTAL :
- kind::BITVECTOR_UREM_TOTAL, num, den);
- Node node = nm->mkNode(kind::ITE, den_eq_0, divByZeroNum, divTotalNumDen);
- if(!d_smt.d_logic.isTheoryEnabled(THEORY_UF)) {
- d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
- d_smt.d_logic.enableTheory(THEORY_UF);
- d_smt.d_logic.lock();
- }
- return node;
-}
Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashFunction>& cache)
stack< triple<Node, Node, bool> > worklist;
stack<Node> result;
worklist.push(make_triple(Node(n), Node(n), false));
+ // The worklist is made of triples, each is input / original node then the output / rewritten node
+ // and finally a flag tracking whether the children have been explored (i.e. if this is a downward
+ // or upward pass).
do {
- n = worklist.top().first;
- Node node = worklist.top().second;
+ n = worklist.top().first; // n is the input / original
+ Node node = worklist.top().second; // node is the output / result
bool childrenPushed = worklist.top().third;
worklist.pop();
+ // Working downwards
if(!childrenPushed) {
Kind k = n.getKind();
+ // Apart from apply, we can short circuit leaves
if(k != kind::APPLY && n.getNumChildren() == 0) {
- SmtEngine::DefinedFunctionMap::const_iterator i = d_smt.d_definedFunctions->find(n);
- if(i != d_smt.d_definedFunctions->end()) {
- // replacement must be closed
- if((*i).second.getFormals().size() > 0) {
- result.push(d_smt.d_nodeManager->mkNode(kind::LAMBDA, d_smt.d_nodeManager->mkNode(kind::BOUND_VAR_LIST, (*i).second.getFormals()), (*i).second.getFormula()));
- continue;
- }
- // don't bother putting in the cache
- result.push((*i).second.getFormula());
- continue;
- }
- // don't bother putting in the cache
- result.push(n);
- continue;
+ SmtEngine::DefinedFunctionMap::const_iterator i = d_smt.d_definedFunctions->find(n);
+ if(i != d_smt.d_definedFunctions->end()) {
+ // replacement must be closed
+ if((*i).second.getFormals().size() > 0) {
+ result.push(d_smt.d_nodeManager->mkNode(kind::LAMBDA, d_smt.d_nodeManager->mkNode(kind::BOUND_VAR_LIST, (*i).second.getFormals()), (*i).second.getFormula()));
+ continue;
+ }
+ // don't bother putting in the cache
+ result.push((*i).second.getFormula());
+ continue;
+ }
+ // don't bother putting in the cache
+ result.push(n);
+ continue;
}
// maybe it's in the cache
}
// otherwise expand it
-
- NodeManager* nm = d_smt.d_nodeManager;
- // FIXME: this theory-specific code should be factored out of the
- // SmtEngine, somehow
- switch(k) {
- case kind::BITVECTOR_SDIV:
- case kind::BITVECTOR_SREM:
- case kind::BITVECTOR_SMOD:
- node = bv::TheoryBVRewriter::eliminateBVSDiv(node);
- break;
-
- case kind::BITVECTOR_UDIV:
- case kind::BITVECTOR_UREM:
- node = expandBVDivByZero(node);
- break;
-
- case kind::STRING_CHARAT: {
- if(d_ufSubstr.isNull()) {
- std::vector< TypeNode > argTypes;
- argTypes.push_back(NodeManager::currentNM()->stringType());
- argTypes.push_back(NodeManager::currentNM()->integerType());
- argTypes.push_back(NodeManager::currentNM()->integerType());
- d_ufSubstr = NodeManager::currentNM()->mkSkolem("__ufSS",
- NodeManager::currentNM()->mkFunctionType(
- argTypes, NodeManager::currentNM()->stringType()),
- "uf substr",
- NodeManager::SKOLEM_EXACT_NAME);
- }
- Node lenxgti = NodeManager::currentNM()->mkNode( kind::GT,
- NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[0] ), n[1] );
- Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );
- Node t1greq0 = NodeManager::currentNM()->mkNode( kind::GEQ, n[1], zero);
- Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1greq0 ));
- Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
- Node totalf = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, n[0], n[1], one);
- Node uf = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, n[0], n[1], one);
- node = NodeManager::currentNM()->mkNode( kind::ITE, cond, totalf, uf );
- break;
- }
- case kind::STRING_SUBSTR: {
- if(d_ufSubstr.isNull()) {
- std::vector< TypeNode > argTypes;
- argTypes.push_back(NodeManager::currentNM()->stringType());
- argTypes.push_back(NodeManager::currentNM()->integerType());
- argTypes.push_back(NodeManager::currentNM()->integerType());
- d_ufSubstr = NodeManager::currentNM()->mkSkolem("__ufSS",
- NodeManager::currentNM()->mkFunctionType(
- argTypes, NodeManager::currentNM()->stringType()),
- "uf substr",
- NodeManager::SKOLEM_EXACT_NAME);
- }
- Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ,
- NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[0] ),
- NodeManager::currentNM()->mkNode( kind::PLUS, n[1], n[2] ) );
- Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );
- Node t1geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, n[1], zero);
- Node t2geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, n[2], zero);
- Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 ));
- Node totalf = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, n[0], n[1], n[2]);
- Node uf = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, n[0], n[1], n[2]);
- node = NodeManager::currentNM()->mkNode( kind::ITE, cond, totalf, uf );
- break;
- }
- case kind::DIVISION: {
- // partial function: division
- if(d_divByZero.isNull()) {
- d_divByZero = nm->mkSkolem("divByZero", nm->mkFunctionType(nm->realType(), nm->realType()),
- "partial real division", NodeManager::SKOLEM_EXACT_NAME);
- if(!d_smt.d_logic.isTheoryEnabled(THEORY_UF)) {
- d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
- d_smt.d_logic.enableTheory(THEORY_UF);
- d_smt.d_logic.lock();
- }
- }
- TNode num = n[0], den = n[1];
- Node den_eq_0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0)));
- Node divByZeroNum = nm->mkNode(kind::APPLY_UF, d_divByZero, num);
- Node divTotalNumDen = nm->mkNode(kind::DIVISION_TOTAL, num, den);
- node = nm->mkNode(kind::ITE, den_eq_0, divByZeroNum, divTotalNumDen);
- break;
- }
-
- case kind::INTS_DIVISION: {
- // partial function: integer div
- if(d_intDivByZero.isNull()) {
- d_intDivByZero = nm->mkSkolem("intDivByZero", nm->mkFunctionType(nm->integerType(), nm->integerType()),
- "partial integer division", NodeManager::SKOLEM_EXACT_NAME);
- if(!d_smt.d_logic.isTheoryEnabled(THEORY_UF)) {
- d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
- d_smt.d_logic.enableTheory(THEORY_UF);
- d_smt.d_logic.lock();
- }
- }
- TNode num = n[0], den = n[1];
- Node den_eq_0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0)));
- Node intDivByZeroNum = nm->mkNode(kind::APPLY_UF, d_intDivByZero, num);
- Node intDivTotalNumDen = nm->mkNode(kind::INTS_DIVISION_TOTAL, num, den);
- node = nm->mkNode(kind::ITE, den_eq_0, intDivByZeroNum, intDivTotalNumDen);
- break;
- }
-
- case kind::INTS_MODULUS: {
- // partial function: mod
- if(d_modZero.isNull()) {
- d_modZero = nm->mkSkolem("modZero", nm->mkFunctionType(nm->integerType(), nm->integerType()),
- "partial modulus", NodeManager::SKOLEM_EXACT_NAME);
- if(!d_smt.d_logic.isTheoryEnabled(THEORY_UF)) {
- d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
- d_smt.d_logic.enableTheory(THEORY_UF);
- d_smt.d_logic.lock();
- }
- }
- TNode num = n[0], den = n[1];
- Node den_eq_0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0)));
- Node modZeroNum = nm->mkNode(kind::APPLY_UF, d_modZero, num);
- Node modTotalNumDen = nm->mkNode(kind::INTS_MODULUS_TOTAL, num, den);
- node = nm->mkNode(kind::ITE, den_eq_0, modZeroNum, modTotalNumDen);
- break;
- }
-
- case kind::ABS: {
- Node out = nm->mkNode(kind::ITE, nm->mkNode(kind::LT, node[0], nm->mkConst(Rational(0))), nm->mkNode(kind::UMINUS, node[0]), node[0]);
- cache[n] = out;
- result.push(out);
- continue;
- }
-
- case kind::APPLY: {
+ if (k == kind::APPLY) {
// application of a user-defined symbol
TNode func = n.getOperator();
SmtEngine::DefinedFunctionMap::const_iterator i =
cache[n] = (n == expanded ? Node::null() : expanded);
result.push(expanded);
continue;
- }
- default:
- // unknown kind for expansion, just iterate over the children
- node = n;
+ } else {
+ theory::Theory* t = d_smt.d_theoryEngine->theoryOf(node);
+
+ Assert(t != NULL);
+ LogicRequest req(d_smt);
+ node = t->expandDefinition(req, n);
}
// there should be children here, otherwise we short-circuited a result-push/continue, above
+ if (node.getNumChildren() == 0) {
+ Debug("expand") << "Unexpectedly no children..." << node << endl;
+ }
+ // This invariant holds at the moment but it is concievable that a new theory
+ // might introduce a kind which can have children before definition expansion but doesn't
+ // afterwards. If this happens, remove this assertion.
Assert(node.getNumChildren() > 0);
// the partial functions can fall through, in which case we still
// consider their children
- worklist.push(make_triple(Node(n), node, true));
+ worklist.push(make_triple(Node(n), node, true)); // Original and rewritten result
for(size_t i = 0; i < node.getNumChildren(); ++i) {
- worklist.push(make_triple(node[i], node[i], false));
+ worklist.push(make_triple(node[i], node[i], false)); // Rewrite the children of the result only
}
} else {
+ // Working upwards
+ // Reconstruct the node from it's (now rewritten) children on the stack
Debug("expand") << "cons : " << node << endl;
//cout << "cons : " << node << endl;
nb << expanded;
}
node = nb;
- cache[n] = n == node ? Node::null() : node;
+ cache[n] = n == node ? Node::null() : node; // Only cache once all subterms are expanded
result.push(node);
}
} while(!worklist.empty());
#include "util/proof.h"
#include "smt/modal_exception.h"
#include "smt/logic_exception.h"
-#include "util/hash.h"
#include "options/options.h"
#include "util/result.h"
#include "util/sexpr.h"
class ProofManager;
class Model;
+class LogicRequest;
class StatisticsRegistry;
namespace context {
friend ::CVC4::StatisticsRegistry* ::CVC4::stats::getStatisticsRegistry(SmtEngine*);
friend void ::CVC4::smt::beforeSearch(std::string, bool, SmtEngine*) throw(ModalException);
friend ProofManager* ::CVC4::smt::currentProofManager();
+ friend class ::CVC4::LogicRequest;
// to access d_modelCommands
friend class ::CVC4::Model;
friend class ::CVC4::theory::TheoryModel;
d_internal->preRegisterTerm(n);
}
+Node TheoryArith::expandDefinition(LogicRequest &logicRequest, Node node) {
+ return d_internal->expandDefinition(logicRequest, node);
+}
+
void TheoryArith::setMasterEqualityEngine(eq::EqualityEngine* eq) {
d_internal->setMasterEqualityEngine(eq);
}
*/
void preRegisterTerm(TNode n);
+ Node expandDefinition(LogicRequest &logicRequest, Node node);
+
void setMasterEqualityEngine(eq::EqualityEngine* eq);
void setQuantifiersEngine(QuantifiersEngine* qe);
#include "util/statistics_registry.h"
#include "util/result.h"
+#include "smt/logic_request.h"
#include "smt/logic_exception.h"
#include "theory/arith/arithvar.h"
return d_rowTracking[ridx];
}
+Node TheoryArithPrivate::expandDefinition(LogicRequest &logicRequest, Node node) {
+ NodeManager* nm = NodeManager::currentNM();
+
+ switch(node.getKind()) {
+ case kind::DIVISION: {
+ // partial function: division
+ if(d_divByZero.isNull()) {
+ d_divByZero = nm->mkSkolem("divByZero", nm->mkFunctionType(nm->realType(), nm->realType()),
+ "partial real division", NodeManager::SKOLEM_EXACT_NAME);
+ logicRequest.widenLogic(THEORY_UF);
+ }
+ TNode num = node[0], den = node[1];
+ Node den_eq_0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0)));
+ Node divByZeroNum = nm->mkNode(kind::APPLY_UF, d_divByZero, num);
+ Node divTotalNumDen = nm->mkNode(kind::DIVISION_TOTAL, num, den);
+ return nm->mkNode(kind::ITE, den_eq_0, divByZeroNum, divTotalNumDen);
+ break;
+ }
+
+ case kind::INTS_DIVISION: {
+ // partial function: integer div
+ if(d_intDivByZero.isNull()) {
+ d_intDivByZero = nm->mkSkolem("intDivByZero", nm->mkFunctionType(nm->integerType(), nm->integerType()),
+ "partial integer division", NodeManager::SKOLEM_EXACT_NAME);
+ logicRequest.widenLogic(THEORY_UF);
+ }
+ TNode num = node[0], den = node[1];
+ Node den_eq_0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0)));
+ Node intDivByZeroNum = nm->mkNode(kind::APPLY_UF, d_intDivByZero, num);
+ Node intDivTotalNumDen = nm->mkNode(kind::INTS_DIVISION_TOTAL, num, den);
+ return nm->mkNode(kind::ITE, den_eq_0, intDivByZeroNum, intDivTotalNumDen);
+ break;
+ }
+
+ case kind::INTS_MODULUS: {
+ // partial function: mod
+ if(d_modZero.isNull()) {
+ d_modZero = nm->mkSkolem("modZero", nm->mkFunctionType(nm->integerType(), nm->integerType()),
+ "partial modulus", NodeManager::SKOLEM_EXACT_NAME);
+ logicRequest.widenLogic(THEORY_UF);
+ }
+ TNode num = node[0], den = node[1];
+ Node den_eq_0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0)));
+ Node modZeroNum = nm->mkNode(kind::APPLY_UF, d_modZero, num);
+ Node modTotalNumDen = nm->mkNode(kind::INTS_MODULUS_TOTAL, num, den);
+ return nm->mkNode(kind::ITE, den_eq_0, modZeroNum, modTotalNumDen);
+ break;
+ }
+
+ case kind::ABS: {
+ return nm->mkNode(kind::ITE, nm->mkNode(kind::LT, node[0], nm->mkConst(Rational(0))), nm->mkNode(kind::UMINUS, node[0]), node[0]);
+ break;
+ }
+
+ default:
+ return node;
+ break;
+ }
+
+ Unreachable();
+}
+
+
}/* CVC4::theory::arith namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
* Does non-context dependent setup for a node connected to a theory.
*/
void preRegisterTerm(TNode n);
+ Node expandDefinition(LogicRequest &logicRequest, Node node);
void setMasterEqualityEngine(eq::EqualityEngine* eq);
void setQuantifiersEngine(QuantifiersEngine* qe);
Statistics d_statistics;
+ /**
+ * Function symbol used to implement uninterpreted division-by-zero
+ * semantics. Needed to deal with partial division function ("/").
+ */
+ Node d_divByZero;
+
+ /**
+ * Function symbol used to implement uninterpreted
+ * int-division-by-zero semantics. Needed to deal with partial
+ * function "div".
+ */
+ Node d_intDivByZero;
+
+ /**
+ * Function symbol used to implement uninterpreted mod-zero
+ * semantics. Needed to deal with partial function "mod".
+ */
+ Node d_modZero;
+
+
};/* class TheoryArithPrivate */
}/* CVC4::theory::arith namespace */
#include "theory/bv/bv_subtheory_core.h"
#include "theory/bv/bv_subtheory_inequality.h"
#include "theory/bv/bv_subtheory_bitblast.h"
+#include "theory/bv/theory_bv_rewriter.h"
#include "theory/theory_model.h"
using namespace CVC4;
StatisticsRegistry::unregisterStat(&d_weightComputationTimer);
}
+Node TheoryBV::getBVDivByZero(Kind k, unsigned width) {
+ NodeManager* nm = NodeManager::currentNM();
+ if (k == kind::BITVECTOR_UDIV) {
+ if (d_BVDivByZero.find(width) == d_BVDivByZero.end()) {
+ // lazily create the function symbols
+ ostringstream os;
+ os << "BVUDivByZero_" << width;
+ Node divByZero = nm->mkSkolem(os.str(),
+ nm->mkFunctionType(nm->mkBitVectorType(width), nm->mkBitVectorType(width)),
+ "partial bvudiv", NodeManager::SKOLEM_EXACT_NAME);
+ d_BVDivByZero[width] = divByZero;
+ }
+ return d_BVDivByZero[width];
+ }
+ else if (k == kind::BITVECTOR_UREM) {
+ if (d_BVRemByZero.find(width) == d_BVRemByZero.end()) {
+ ostringstream os;
+ os << "BVURemByZero_" << width;
+ Node divByZero = nm->mkSkolem(os.str(),
+ nm->mkFunctionType(nm->mkBitVectorType(width), nm->mkBitVectorType(width)),
+ "partial bvurem", NodeManager::SKOLEM_EXACT_NAME);
+ d_BVRemByZero[width] = divByZero;
+ }
+ return d_BVRemByZero[width];
+ }
+
+ Unreachable();
+}
+
+
+Node TheoryBV::expandDefinition(LogicRequest &logicRequest, Node node) {
+ Debug("bitvector-expandDefinition") << "TheoryBV::expandDefinition(" << node << ")" << std::endl;
+
+ switch (node.getKind()) {
+ case kind::BITVECTOR_SDIV:
+ case kind::BITVECTOR_SREM:
+ case kind::BITVECTOR_SMOD:
+ return TheoryBVRewriter::eliminateBVSDiv(node);
+ break;
+
+ case kind::BITVECTOR_UDIV:
+ case kind::BITVECTOR_UREM: {
+ NodeManager* nm = NodeManager::currentNM();
+ unsigned width = node.getType().getBitVectorSize();
+ Node divByZero = getBVDivByZero(node.getKind(), width);
+ TNode num = node[0], den = node[1];
+ Node den_eq_0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(BitVector(width, Integer(0))));
+ Node divByZeroNum = nm->mkNode(kind::APPLY_UF, divByZero, num);
+ Node divTotalNumDen = nm->mkNode(node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_UDIV_TOTAL :
+ kind::BITVECTOR_UREM_TOTAL, num, den);
+ node = nm->mkNode(kind::ITE, den_eq_0, divByZeroNum, divTotalNumDen);
+ logicRequest.widenLogic(THEORY_UF);
+ return node;
+ }
+ break;
+
+ default:
+ return node;
+ break;
+ }
+
+ Unreachable();
+}
void TheoryBV::preRegisterTerm(TNode node) {
#include "context/cdhashset.h"
#include "theory/bv/theory_bv_utils.h"
#include "util/statistics_registry.h"
+#include "util/hash.h"
#include "theory/bv/bv_subtheory.h"
namespace CVC4 {
std::vector<SubtheorySolver*> d_subtheories;
__gnu_cxx::hash_map<SubTheory, SubtheorySolver*, std::hash<int> > d_subtheoryMap;
+
+
public:
TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
void setMasterEqualityEngine(eq::EqualityEngine* eq);
+ Node expandDefinition(LogicRequest &logicRequest, Node node);
+
void preRegisterTerm(TNode n);
void check(Effort e);
Statistics d_statistics;
+
+ /**
+ * Return the uinterpreted function symbol corresponding to division-by-zero
+ * for this particular bit-width
+ * @param k should be UREM or UDIV
+ * @param width
+ *
+ * @return
+ */
+ Node getBVDivByZero(Kind k, unsigned width);
+
+ /**
+ * Maps from bit-vector width to divison-by-zero uninterpreted
+ * function symbols.
+ */
+ __gnu_cxx::hash_map<unsigned, Node> d_BVDivByZero;
+ __gnu_cxx::hash_map<unsigned, Node> d_BVRemByZero;
+
+
context::CDO<bool> d_lemmasAdded;
// Are we in conflict?
}
}
+Node TheoryStrings::expandDefinition(LogicRequest &logicRequest, Node node) {
+ switch (node.getKind()) {
+ case kind::STRING_CHARAT: {
+ if(d_ufSubstr.isNull()) {
+ std::vector< TypeNode > argTypes;
+ argTypes.push_back(NodeManager::currentNM()->stringType());
+ argTypes.push_back(NodeManager::currentNM()->integerType());
+ argTypes.push_back(NodeManager::currentNM()->integerType());
+ d_ufSubstr = NodeManager::currentNM()->mkSkolem("__ufSS",
+ NodeManager::currentNM()->mkFunctionType(
+ argTypes, NodeManager::currentNM()->stringType()),
+ "uf substr",
+ NodeManager::SKOLEM_EXACT_NAME);
+ }
+ Node lenxgti = NodeManager::currentNM()->mkNode( kind::GT,
+ NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, node[0] ), node[1] );
+ Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );
+ Node t1greq0 = NodeManager::currentNM()->mkNode( kind::GEQ, node[1], zero);
+ Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1greq0 ));
+ Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
+ Node totalf = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, node[0], node[1], one);
+ Node uf = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, node[0], node[1], one);
+ return NodeManager::currentNM()->mkNode( kind::ITE, cond, totalf, uf );
+ }
+ break;
+
+ case kind::STRING_SUBSTR: {
+ if(d_ufSubstr.isNull()) {
+ std::vector< TypeNode > argTypes;
+ argTypes.push_back(NodeManager::currentNM()->stringType());
+ argTypes.push_back(NodeManager::currentNM()->integerType());
+ argTypes.push_back(NodeManager::currentNM()->integerType());
+ d_ufSubstr = NodeManager::currentNM()->mkSkolem("__ufSS",
+ NodeManager::currentNM()->mkFunctionType(
+ argTypes, NodeManager::currentNM()->stringType()),
+ "uf substr",
+ NodeManager::SKOLEM_EXACT_NAME);
+ }
+ Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ,
+ NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, node[0] ),
+ NodeManager::currentNM()->mkNode( kind::PLUS, node[1], node[2] ) );
+ Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );
+ Node t1geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, node[1], zero);
+ Node t2geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, node[2], zero);
+ Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 ));
+ Node totalf = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, node[0], node[1], node[2]);
+ Node uf = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, node[0], node[1], node[2]);
+ return NodeManager::currentNM()->mkNode( kind::ITE, cond, totalf, uf );
+ }
+ break;
+
+ default :
+ return node;
+ break;
+ }
+
+ Unreachable();
+}
+
+
void TheoryStrings::check(Effort e) {
//Assert( d_pending.empty() );
};/* class TheoryStrings::NotifyClass */
private:
+ /**
+ * Function symbol used to implement uninterpreted undefined string
+ * semantics. Needed to deal with partial charat/substr function.
+ */
+ Node d_ufSubstr;
+
+ /**
+ * Function symbol used to implement uninterpreted undefined string
+ * semantics. Needed to deal with partial str2int function.
+ */
+ Node d_ufS2I;
+
// Constants
Node d_emptyString;
Node d_emptyRegexp;
public:
void preRegisterTerm(TNode n);
+ Node expandDefinition(LogicRequest &logicRequest, Node n);
void check(Effort e);
/** Conflict when merging two constants */
#include "expr/node.h"
//#include "expr/attribute.h"
#include "expr/command.h"
+#include "smt/logic_request.h"
#include "theory/valuation.h"
#include "theory/output_channel.h"
#include "theory/logic_info.h"
*/
virtual void finishInit() { }
+ /**
+ * Some theories have kinds that are effectively definitions and
+ * should be expanded before they are handled. Definitions allow
+ * a much wider range of actions than the normal forms given by the
+ * rewriter; they can enable other theories and create new terms.
+ * However no assumptions can be made about subterms having been
+ * expanded or rewritten. Where possible rewrite rules should be
+ * used, definitions should only be used when rewrites are not
+ * possible, for example in handling under-specified operations
+ * using partially defined functions.
+ */
+ virtual Node expandDefinition(LogicRequest &logicRequest, Node node) {
+ // by default, do nothing
+ return node;
+ }
+
/**
* Pre-register a term. Done one time for a Node, ever.
*/
projects / cvc5.git / commitdiff