From 9d855960ba88c9b476ab1be17b7686c009f516f5 Mon Sep 17 00:00:00 2001 From: Martin Brain <> Date: Tue, 11 Mar 2014 00:03:41 +0000 Subject: [PATCH] Refactor the theory specific parts of definition expansion into the theory solvers. 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 --- src/Makefile.am | 1 + src/smt/logic_request.h | 53 ++++ src/smt/smt_engine.cpp | 302 +++------------------- src/smt/smt_engine.h | 3 +- src/theory/arith/theory_arith.cpp | 4 + src/theory/arith/theory_arith.h | 2 + src/theory/arith/theory_arith_private.cpp | 64 +++++ src/theory/arith/theory_arith_private.h | 21 ++ src/theory/bv/theory_bv.cpp | 64 +++++ src/theory/bv/theory_bv.h | 24 ++ src/theory/strings/theory_strings.cpp | 60 +++++ src/theory/strings/theory_strings.h | 13 + src/theory/theory.h | 17 ++ 13 files changed, 366 insertions(+), 262 deletions(-) create mode 100644 src/smt/logic_request.h diff --git a/src/Makefile.am b/src/Makefile.am index 03092979a..d75535e15 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -116,6 +116,7 @@ libcvc4_la_SOURCES = \ 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 \ diff --git a/src/smt/logic_request.h b/src/smt/logic_request.h new file mode 100644 index 000000000..4985b0e65 --- /dev/null +++ b/src/smt/logic_request.h @@ -0,0 +1,53 @@ +/********************* */ +/*! \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 */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 911a16eed..328a20c28 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -43,6 +43,7 @@ #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" @@ -308,44 +309,6 @@ class SmtEnginePrivate : public NodeManagerListener { */ hash_map 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 d_BVDivByZero; - hash_map 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; @@ -448,9 +411,6 @@ public: d_fakeContext(), d_abstractValueMap(&d_fakeContext), d_abstractValues(), - d_divByZero(), - d_intDivByZero(), - d_modZero(), d_simplifyAssertionsDepth(0), d_iteSkolemMap(), d_iteRemover(smt.d_userContext), @@ -553,25 +513,6 @@ public: 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. */ @@ -1002,7 +943,7 @@ void SmtEngine::setDefaults() { 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; @@ -1518,55 +1459,6 @@ void SmtEngine::defineFunction(Expr func, } -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& cache) @@ -1575,31 +1467,36 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map > worklist; stack 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 @@ -1611,134 +1508,7 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map 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 = @@ -1777,25 +1547,35 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_maptheoryOf(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; @@ -1814,7 +1594,7 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_mappreRegisterTerm(n); } +Node TheoryArith::expandDefinition(LogicRequest &logicRequest, Node node) { + return d_internal->expandDefinition(logicRequest, node); +} + void TheoryArith::setMasterEqualityEngine(eq::EqualityEngine* eq) { d_internal->setMasterEqualityEngine(eq); } diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 428c101a6..eaa9a98c6 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -53,6 +53,8 @@ public: */ void preRegisterTerm(TNode n); + Node expandDefinition(LogicRequest &logicRequest, Node node); + void setMasterEqualityEngine(eq::EqualityEngine* eq); void setQuantifiersEngine(QuantifiersEngine* qe); diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 37dba5e92..a63de446c 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -38,6 +38,7 @@ #include "util/statistics_registry.h" #include "util/result.h" +#include "smt/logic_request.h" #include "smt/logic_exception.h" #include "theory/arith/arithvar.h" @@ -4620,6 +4621,69 @@ const BoundsInfo& TheoryArithPrivate::boundsInfo(ArithVar basic) const{ 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 */ diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 33c588ed4..68e839ef8 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -397,6 +397,7 @@ public: * 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); @@ -772,6 +773,26 @@ private: 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 */ diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 6daf99c8b..5d5e0a97c 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -25,6 +25,7 @@ #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; @@ -102,6 +103,69 @@ TheoryBV::Statistics::~Statistics() { 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) { diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 3d093c861..a5e2ac9ea 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -25,6 +25,7 @@ #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 { @@ -46,6 +47,8 @@ class TheoryBV : public Theory { std::vector d_subtheories; __gnu_cxx::hash_map > d_subtheoryMap; + + public: TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); @@ -53,6 +56,8 @@ public: void setMasterEqualityEngine(eq::EqualityEngine* eq); + Node expandDefinition(LogicRequest &logicRequest, Node node); + void preRegisterTerm(TNode n); void check(Effort e); @@ -85,6 +90,25 @@ private: 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 d_BVDivByZero; + __gnu_cxx::hash_map d_BVRemByZero; + + context::CDO d_lemmasAdded; // Are we in conflict? diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index a4d3145d9..c44d2d334 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -463,6 +463,66 @@ void TheoryStrings::preRegisterTerm(TNode n) { } } +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() ); diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 902b902b6..e07c61a19 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -112,6 +112,18 @@ public: };/* 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; @@ -241,6 +253,7 @@ private: public: void preRegisterTerm(TNode n); + Node expandDefinition(LogicRequest &logicRequest, Node n); void check(Effort e); /** Conflict when merging two constants */ diff --git a/src/theory/theory.h b/src/theory/theory.h index e8d53e539..42cdea280 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -22,6 +22,7 @@ #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" @@ -480,6 +481,22 @@ public: */ 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. */ -- 2.30.2