diff options
author | lianah <lianahady@gmail.com> | 2013-03-26 22:14:24 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-03-26 22:14:24 -0400 |
commit | 2bed73156740d7e93e303b02319c407a1d587109 (patch) | |
tree | 99876e3263f20b0c507caac27c147a991fc759dd /src/theory | |
parent | 33a5c0897bdbfb8367dfa90342471615908df1bc (diff) | |
parent | 70d1a0171840cd62b5c1d89b875ffb50da216793 (diff) |
added model generation for bv subtheories and bv-inequality solver option
Diffstat (limited to 'src/theory')
29 files changed, 418 insertions, 31 deletions
diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index b30a399e4..b3760b239 100644 --- a/src/theory/Makefile.am +++ b/src/theory/Makefile.am @@ -3,7 +3,7 @@ AM_CPPFLAGS = \ -I@builddir@/.. -I@srcdir@/../include -I@srcdir@/.. AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -SUBDIRS = builtin booleans uf arith arrays bv datatypes quantifiers rewriterules +SUBDIRS = builtin booleans uf arith bv arrays datatypes quantifiers rewriterules DIST_SUBDIRS = $(SUBDIRS) example noinst_LTLIBRARIES = libtheory.la diff --git a/src/theory/booleans/Makefile.am b/src/theory/booleans/Makefile.am index 8cb32de18..9d58ffa75 100644 --- a/src/theory/booleans/Makefile.am +++ b/src/theory/booleans/Makefile.am @@ -13,7 +13,10 @@ libbooleans_la_SOURCES = \ theory_bool_rewriter.h \ theory_bool_rewriter.cpp \ circuit_propagator.h \ - circuit_propagator.cpp + circuit_propagator.cpp \ + boolean_term_conversion_mode.h \ + boolean_term_conversion_mode.cpp EXTRA_DIST = \ - kinds + kinds \ + options_handlers.h diff --git a/src/theory/booleans/boolean_term_conversion_mode.cpp b/src/theory/booleans/boolean_term_conversion_mode.cpp new file mode 100644 index 000000000..f9d80835c --- /dev/null +++ b/src/theory/booleans/boolean_term_conversion_mode.cpp @@ -0,0 +1,41 @@ +/********************* */ +/*! \file boolean_term_conversion_mode.cpp + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include <iostream> +#include "theory/booleans/boolean_term_conversion_mode.h" + +namespace CVC4 { + +std::ostream& operator<<(std::ostream& out, theory::booleans::BooleanTermConversionMode mode) { + switch(mode) { + case theory::booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS: + out << "BOOLEAN_TERM_CONVERT_TO_BITVECTORS"; + break; + case theory::booleans::BOOLEAN_TERM_CONVERT_TO_DATATYPES: + out << "BOOLEAN_TERM_CONVERT_TO_DATATYPES"; + break; + case theory::booleans::BOOLEAN_TERM_CONVERT_NATIVE: + out << "BOOLEAN_TERM_CONVERT_NATIVE"; + break; + default: + out << "BooleanTermConversionMode!UNKNOWN"; + } + + return out; +} + +}/* CVC4 namespace */ diff --git a/src/theory/booleans/boolean_term_conversion_mode.h b/src/theory/booleans/boolean_term_conversion_mode.h new file mode 100644 index 000000000..6ca908df4 --- /dev/null +++ b/src/theory/booleans/boolean_term_conversion_mode.h @@ -0,0 +1,53 @@ +/********************* */ +/*! \file boolean_term_conversion_mode.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): mdeters + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__BOOLEANS__BOOLEAN_TERM_CONVERSION_MODE_H +#define __CVC4__THEORY__BOOLEANS__BOOLEAN_TERM_CONVERSION_MODE_H + +#include <iostream> + +namespace CVC4 { +namespace theory { +namespace booleans { + +typedef enum { + /** + * Convert Boolean terms to bitvectors of size 1. + */ + BOOLEAN_TERM_CONVERT_TO_BITVECTORS, + /** + * Convert Boolean terms to enumerations in the Datatypes theory. + */ + BOOLEAN_TERM_CONVERT_TO_DATATYPES, + /** + * Convert Boolean terms to enumerations in the Datatypes theory IF + * used in a datatypes context, otherwise to a bitvector of size 1. + */ + BOOLEAN_TERM_CONVERT_NATIVE + +} BooleanTermConversionMode; + +}/* CVC4::theory::booleans namespace */ +}/* CVC4::theory namespace */ + +std::ostream& operator<<(std::ostream& out, theory::booleans::BooleanTermConversionMode mode) CVC4_PUBLIC; + +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__BOOLEANS__BOOLEAN_TERM_CONVERSION_MODE_H */ diff --git a/src/theory/booleans/options b/src/theory/booleans/options index ae14de58b..6c571f30e 100644 --- a/src/theory/booleans/options +++ b/src/theory/booleans/options @@ -5,4 +5,7 @@ module BOOLEANS "theory/booleans/options.h" Boolean theory +option booleanTermConversionMode boolean-term-conversion-mode --boolean-term-conversion-mode=MODE CVC4::theory::booleans::BooleanTermConversionMode :default CVC4::theory::booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS :include "theory/booleans/boolean_term_conversion_mode.h" :handler CVC4::theory::booleans::stringToBooleanTermConversionMode :handler-include "theory/booleans/options_handlers.h" + policy for converting Boolean terms + endmodule diff --git a/src/theory/booleans/options_handlers.h b/src/theory/booleans/options_handlers.h new file mode 100644 index 000000000..2bf53b3d2 --- /dev/null +++ b/src/theory/booleans/options_handlers.h @@ -0,0 +1,65 @@ +/********************* */ +/*! \file options_handlers.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__BOOLEANS__OPTIONS_HANDLERS_H +#define __CVC4__THEORY__BOOLEANS__OPTIONS_HANDLERS_H + +#include <string> + +namespace CVC4 { +namespace theory { +namespace booleans { + +static const std::string booleanTermConversionModeHelp = "\ +Boolean term conversion modes currently supported by the\n\ +--boolean-term-conversion-mode option:\n\ +\n\ +bitvectors [default]\n\ ++ Boolean terms are converted to bitvectors of size 1.\n\ +\n\ +datatypes\n\ ++ Boolean terms are converted to enumerations in the Datatype theory.\n\ +\n\ +native\n\ ++ Boolean terms are converted in a \"natural\" way depending on where they\n\ + are used. If in a datatype context, they are converted to an enumeration.\n\ + Elsewhere, they are converted to a bitvector of size 1.\n\ +"; + +inline BooleanTermConversionMode stringToBooleanTermConversionMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { + if(optarg == "bitvectors") { + return BOOLEAN_TERM_CONVERT_TO_BITVECTORS; + } else if(optarg == "datatypes") { + return BOOLEAN_TERM_CONVERT_TO_DATATYPES; + } else if(optarg == "native") { + return BOOLEAN_TERM_CONVERT_NATIVE; + } else if(optarg == "help") { + puts(booleanTermConversionModeHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --boolean-term-conversion-mode: `") + + optarg + "'. Try --boolean-term-conversion-mode help."); + } +} + +}/* CVC4::theory::booleans namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__BOOLEANS__OPTIONS_HANDLERS_H */ diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 352868f7b..a369fb572 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -79,7 +79,7 @@ class EqualityTypeRule { if ( TypeNode::leastCommonTypeNode(lhsType, rhsType).isNull() ) { std::stringstream ss; - ss << "Subtypes must have a common type:" << std::endl; + ss << "Subexpressions must have a common base type:" << std::endl; ss << "Equation: " << n << std::endl; ss << "Type 1: " << lhsType << std::endl; ss << "Type 2: " << rhsType << std::endl; diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp index cc589c5c3..6da3b8efc 100644 --- a/src/theory/bv/bitblaster.cpp +++ b/src/theory/bv/bitblaster.cpp @@ -438,7 +438,7 @@ Node Bitblaster::getVarValue(TNode a) { if (d_cnfStream->hasLiteral(bits[i])) { SatLiteral bit = d_cnfStream->getLiteral(bits[i]); bit_value = d_satSolver->value(bit); - Assert (bit_value != SAT_VALUE_UNKNOWN); + Assert (bit_value != SAT_VALUE_UNKNOWN); } else { // the bit is unconstrainted so we can give it an arbitrary value bit_value = SAT_VALUE_FALSE; @@ -453,7 +453,7 @@ void Bitblaster::collectModelInfo(TheoryModel* m) { __gnu_cxx::hash_set<TNode, TNodeHashFunction>::iterator it = d_variables.begin(); for (; it!= d_variables.end(); ++it) { TNode var = *it; - if ((Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var)) && hasValue(var)) { + if (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var)) { Node const_value = getVarValue(var); Debug("bitvector-model") << "Bitblaster::collectModelInfo (assert (= " << var << " " diff --git a/src/theory/bv/bv_inequality_graph.cpp b/src/theory/bv/bv_inequality_graph.cpp index 3dfeba140..6d2ed0cf6 100644 --- a/src/theory/bv/bv_inequality_graph.cpp +++ b/src/theory/bv/bv_inequality_graph.cpp @@ -458,3 +458,15 @@ BitVector InequalityGraph::getValueInModel(TNode node) const { Assert (hasModelValue(id)); return getValue(id); } + +void InequalityGraph::getAllValuesInModel(std::vector<Node>& assignments) { + for (ModelValues::const_iterator it = d_modelValues.begin(); it != d_modelValues.end(); ++it) { + TermId id = (*it).first; + BitVector value = (*it).second.value; + TNode var = getTermNode(id); + Node constant = utils::mkConst(value); + Node assignment = utils::mkNode(kind::EQUAL, var, constant); + assignments.push_back(assignment); + Debug("bitvector-model") << " " << var <<" => " << constant << "\n"; + } +} diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h index b23ea7704..860302aa4 100644 --- a/src/theory/bv/bv_inequality_graph.h +++ b/src/theory/bv/bv_inequality_graph.h @@ -88,11 +88,11 @@ class InequalityGraph : public context::ContextNotifyObj{ {} }; - typedef context::CDHashMap<TermId, ModelValue> Model; + typedef context::CDHashMap<TermId, ModelValue> ModelValues; struct QueueComparator { - const Model* d_model; - QueueComparator(const Model* model) + const ModelValues* d_model; + QueueComparator(const ModelValues* model) : d_model(model) {} bool operator() (TermId left, TermId right) const { @@ -128,7 +128,7 @@ class InequalityGraph : public context::ContextNotifyObj{ std::vector<TNode> d_conflict; bool d_signed; - Model d_modelValues; + ModelValues d_modelValues; void initializeModelValue(TNode node); void setModelValue(TermId term, const ModelValue& mv); ModelValue getModelValue(TermId term) const; @@ -290,7 +290,9 @@ public: * * @return */ - BitVector getValueInModel(TNode a) const; + BitVector getValueInModel(TNode a) const; + + void getAllValuesInModel(std::vector<Node>& assignments); }; } diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h index 4389dc50d..ed90e0ebe 100644 --- a/src/theory/bv/bv_subtheory.h +++ b/src/theory/bv/bv_subtheory.h @@ -91,6 +91,7 @@ public: virtual void preRegister(TNode node) {} virtual void propagate(Theory::Effort e) {} virtual void collectModelInfo(TheoryModel* m) = 0; + virtual Node getModelValue(TNode var) = 0; virtual bool isComplete() = 0; virtual EqualityStatus getEqualityStatus(TNode a, TNode b) = 0; virtual void addSharedTerm(TNode node) {} diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp index c7387daf8..9c4a5c5b6 100644 --- a/src/theory/bv/bv_subtheory_bitblast.cpp +++ b/src/theory/bv/bv_subtheory_bitblast.cpp @@ -64,6 +64,7 @@ void BitblastSolver::explain(TNode literal, std::vector<TNode>& assumptions) { bool BitblastSolver::check(Theory::Effort e) { + Debug("bv-bitblast") << "BitblastSolver::check (" << e << ")\n"; ++(d_statistics.d_numCallstoCheck); //// Eager bit-blasting if (options::bitvectorEagerBitblast()) { @@ -87,7 +88,8 @@ bool BitblastSolver::check(Theory::Effort e) { // Processing assertions while (!done()) { - TNode fact = get(); + TNode fact = get(); + Debug("bv-bitblast") << " fact " << fact << ")\n"; if (!d_bv->inConflict() && (!d_bv->wasPropagatedBySubtheory(fact) || d_bv->getPropagatingSubtheory(fact) != SUB_BITBLAST)) { // Some atoms have not been bit-blasted yet d_bitblaster->bbAtom(fact); @@ -137,3 +139,7 @@ EqualityStatus BitblastSolver::getEqualityStatus(TNode a, TNode b) { void BitblastSolver::collectModelInfo(TheoryModel* m) { return d_bitblaster->collectModelInfo(m); } + +Node BitblastSolver::getModelValue(TNode node) { + return d_bitblaster->getVarValue(node); +} diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h index b05ac74cd..b6be84df5 100644 --- a/src/theory/bv/bv_subtheory_bitblast.h +++ b/src/theory/bv/bv_subtheory_bitblast.h @@ -50,6 +50,7 @@ public: void explain(TNode literal, std::vector<TNode>& assumptions); EqualityStatus getEqualityStatus(TNode a, TNode b); void collectModelInfo(TheoryModel* m); + Node getModelValue(TNode node); bool isComplete() { return true; } }; diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp index 112f73083..15720885d 100644 --- a/src/theory/bv/bv_subtheory_core.cpp +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -222,9 +222,92 @@ bool CoreSolver::check(Theory::Effort e) { // if (!ok) // return false; // } + + // if we are sat and in full check attempt to construct a model + if (Theory::fullEffort(e) && isComplete()) { + buildModel(); + } + return true; } +void CoreSolver::buildModel() { + Debug("bv-core") << "CoreSolver::buildModel() \n"; + d_modelValues.clear(); + TNodeSet constants; + TNodeSet constants_in_eq_engine; + // collect constants in equality engine + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(&d_equalityEngine); + while (!eqcs_i.isFinished()) { + TNode repr = *eqcs_i; + if (repr.getKind() == kind::CONST_BITVECTOR) { + // must check if it's just the constant + eq::EqClassIterator it(repr, &d_equalityEngine); + if (!(++it).isFinished()) { + constants.insert(repr); + constants_in_eq_engine.insert(repr); + } + } + ++eqcs_i; + } + // build repr to value map + + eqcs_i = eq::EqClassesIterator(&d_equalityEngine); + while (!eqcs_i.isFinished()) { + TNode repr = *eqcs_i; + ++eqcs_i; + TypeNode type = repr.getType(); + if (type.isBitVector() && repr.getKind()!= kind::CONST_BITVECTOR) { + Debug("bv-core-model") << " processing " << repr <<"\n"; + // we need to assign a value for it + TypeEnumerator te(type); + Node val; + do { + val = *te; + ++te; + // Debug("bv-core-model") << " trying value " << val << "\n"; + // Debug("bv-core-model") << " is in set? " << constants.count(val) << "\n"; + // Debug("bv-core-model") << " enumerator done? " << te.isFinished() << "\n"; + } while (constants.count(val) != 0 && !(te.isFinished())); + + if (te.isFinished() && constants.count(val) != 0) { + // if we cannot enumerate anymore values we just return the lemma stating that + // at least two of the representatives are equal. + std::vector<TNode> representatives; + representatives.push_back(repr); + + for (TNodeSet::const_iterator it = constants_in_eq_engine.begin(); + it != constants_in_eq_engine.end(); ++it) { + TNode constant = *it; + if (utils::getSize(constant) == utils::getSize(repr)) { + representatives.push_back(constant); + } + } + for (ModelValue::const_iterator it = d_modelValues.begin(); it != d_modelValues.end(); ++it) { + representatives.push_back(it->first); + } + std::vector<Node> equalities; + for (unsigned i = 0; i < representatives.size(); ++i) { + for (unsigned j = i + 1; j < representatives.size(); ++j) { + TNode a = representatives[i]; + TNode b = representatives[j]; + if (utils::getSize(a) == utils::getSize(b)) { + equalities.push_back(utils::mkNode(kind::EQUAL, a, b)); + } + } + } + Node lemma = utils::mkOr(equalities); + d_bv->lemma(lemma); + Debug("bv-core") << " lemma: " << lemma << "\n"; + return; + } + Debug("bv-core-model") << " " << repr << " => " << val <<"\n" ; + constants.insert(val); + d_modelValues[repr] = val; + } + } +} + bool CoreSolver::assertFactToEqualityEngine(TNode fact, TNode reason) { // Notify the equality engine if (d_useEqualityEngine && !d_bv->inConflict() && (!d_bv->wasPropagatedBySubtheory(fact) || !d_bv->getPropagatingSubtheory(fact) == SUB_CORE)) { @@ -297,8 +380,6 @@ void CoreSolver::conflict(TNode a, TNode b) { d_bv->setConflict(conflict); } - - void CoreSolver::collectModelInfo(TheoryModel* m) { if (Debug.isOn("bitvector-model")) { context::CDQueue<Node>::const_iterator it = d_assertionQueue.begin(); @@ -310,6 +391,20 @@ void CoreSolver::collectModelInfo(TheoryModel* m) { set<Node> termSet; d_bv->computeRelevantTerms(termSet); m->assertEqualityEngine(&d_equalityEngine, &termSet); + if (isComplete()) { + Debug("bitvector-model") << "CoreSolver::collectModelInfo complete."; + for (ModelValue::const_iterator it = d_modelValues.begin(); it != d_modelValues.end(); ++it) { + Node a = it->first; + Node b = it->second; + m->assertEquality(a, b, true); + } + } +} + +Node CoreSolver::getModelValue(TNode var) { + Assert (isComplete()); + Assert (d_modelValues.find(var) != d_modelValues.end()); + return d_modelValues[d_equalityEngine.getRepresentative(var)]; } CoreSolver::Statistics::Statistics() diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h index 4a9d84f79..d04dc164f 100644 --- a/src/theory/bv/bv_subtheory_core.h +++ b/src/theory/bv/bv_subtheory_core.h @@ -31,6 +31,9 @@ class Base; * Bitvector equality solver */ class CoreSolver : public SubtheorySolver { + typedef __gnu_cxx::hash_map<TNode, Node, TNodeHashFunction> ModelValue; + typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; + struct Statistics { IntStat d_numCallstoCheck; Statistics(); @@ -69,7 +72,9 @@ class CoreSolver : public SubtheorySolver { Slicer* d_slicer; context::CDO<bool> d_isCoreTheory; /** To make sure we keep the explanations */ - context::CDHashSet<Node, NodeHashFunction> d_reasons; + context::CDHashSet<Node, NodeHashFunction> d_reasons; + ModelValue d_modelValues; + void buildModel(); bool assertFactToEqualityEngine(TNode fact, TNode reason); bool decomposeFact(TNode fact); Node getBaseDecomposition(TNode a, std::vector<TNode>& explanation); @@ -83,6 +88,7 @@ public: bool check(Theory::Effort e); void explain(TNode literal, std::vector<TNode>& assumptions); void collectModelInfo(TheoryModel* m); + Node getModelValue(TNode var); void addSharedTerm(TNode t) { d_equalityEngine.addTriggerTerm(t, THEORY_BV); } diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp index 3d7339e88..27047f6af 100644 --- a/src/theory/bv/bv_subtheory_inequality.cpp +++ b/src/theory/bv/bv_subtheory_inequality.cpp @@ -153,6 +153,23 @@ void InequalitySolver::propagate(Theory::Effort e) { Assert (false); } +void InequalitySolver::collectModelInfo(TheoryModel* m) { + Debug("bitvector-model") << "InequalitySolver::collectModelInfo \n"; + std::vector<Node> model; + d_inequalityGraph.getAllValuesInModel(model); + for (unsigned i = 0; i < model.size(); ++i) { + Assert (model[i].getKind() == kind::EQUAL); + m->assertEquality(model[i][0], model[i][1], true); + } +} + +Node InequalitySolver::getModelValue(TNode var) { + Assert (isComplete()); + Assert (d_inequalityGraph.hasValueInModel(var)); + BitVector val = d_inequalityGraph.getValueInModel(var); + return utils::mkConst(val); +} + InequalitySolver::Statistics::Statistics() : d_numCallstoCheck("theory::bv::InequalitySolver::NumCallsToCheck", 0) { diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h index bcf94dc8b..b19ebb381 100644 --- a/src/theory/bv/bv_subtheory_inequality.h +++ b/src/theory/bv/bv_subtheory_inequality.h @@ -54,7 +54,8 @@ public: void propagate(Theory::Effort e); void explain(TNode literal, std::vector<TNode>& assumptions); bool isComplete() { return d_isComplete; } - void collectModelInfo(TheoryModel* m) {} + void collectModelInfo(TheoryModel* m); + Node getModelValue(TNode var); EqualityStatus getEqualityStatus(TNode a, TNode b); void assertFact(TNode fact); }; diff --git a/src/theory/bv/options b/src/theory/bv/options index 72db63c09..8e01c6572 100644 --- a/src/theory/bv/options +++ b/src/theory/bv/options @@ -14,4 +14,6 @@ option bitvectorShareLemmas --bitblast-share-lemmas bool option bitvectorEagerFullcheck --bitblast-eager-fullcheck bool check the bitblasting eagerly +option bitvectorInequalitySolver --bv-inequality-solver bool + turn on the inequality solver for the bit-vector theory endmodule diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 43e290175..8245fdbdc 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -52,10 +52,12 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& d_subtheories.push_back(core_solver); d_subtheoryMap[SUB_CORE] = core_solver; - SubtheorySolver* ineq_solver = new InequalitySolver(c, this); - d_subtheories.push_back(ineq_solver); - d_subtheoryMap[SUB_INEQUALITY] = ineq_solver; - + if (options::bitvectorInequalitySolver()) { + SubtheorySolver* ineq_solver = new InequalitySolver(c, this); + d_subtheories.push_back(ineq_solver); + d_subtheoryMap[SUB_INEQUALITY] = ineq_solver; + } + SubtheorySolver* bb_solver = new BitblastSolver(c, this); d_subtheories.push_back(bb_solver); d_subtheoryMap[SUB_BITBLAST] = bb_solver; @@ -164,8 +166,21 @@ void TheoryBV::collectModelInfo( TheoryModel* m, bool fullModel ){ Assert(!inConflict()); // Assert (fullModel); // can only query full model for (unsigned i = 0; i < d_subtheories.size(); ++i) { - d_subtheories[i]->collectModelInfo(m); + if (d_subtheories[i]->isComplete()) { + d_subtheories[i]->collectModelInfo(m); + return; + } + } +} + +Node TheoryBV::getModelValue(TNode var) { + Assert(!inConflict()); + for (unsigned i = 0; i < d_subtheories.size(); ++i) { + if (d_subtheories[i]->isComplete()) { + return d_subtheories[i]->getModelValue(var); + } } + Unreachable(); } void TheoryBV::propagate(Effort e) { diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 5d139e11f..6bc4bdaf6 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -125,6 +125,8 @@ private: EqualityStatus getEqualityStatus(TNode a, TNode b); + Node getModelValue(TNode var); + inline std::string indent() { std::string indentStr(getSatContext()->getLevel(), ' '); diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index 98bc8041d..f8b9f010e 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -249,6 +249,32 @@ inline unsigned isPow2Const(TNode node) { typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; +inline Node mkOr(const std::vector<Node>& nodes) { + std::set<TNode> all; + all.insert(nodes.begin(), nodes.end()); + + if (all.size() == 0) { + return mkTrue(); + } + + if (all.size() == 1) { + // All the same, or just one + return nodes[0]; + } + + + NodeBuilder<> disjunction(kind::OR); + std::set<TNode>::const_iterator it = all.begin(); + std::set<TNode>::const_iterator it_end = all.end(); + while (it != it_end) { + disjunction << *it; + ++ it; + } + + return disjunction; +}/* mkOr() */ + + inline Node mkAnd(const std::vector<TNode>& conjunctions) { std::set<TNode> all; all.insert(conjunctions.begin(), conjunctions.end()); diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 9e4f0de75..a3bec7af0 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -24,6 +24,7 @@ #include "theory/datatypes/theory_datatypes_type_rules.h" #include "theory/model.h" #include "smt/options.h" +#include "smt/boolean_terms.h" #include "theory/quantifiers/options.h" #include <map> @@ -311,15 +312,28 @@ Node TheoryDatatypes::ppRewrite(TNode in) { return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, Node::fromExpr(dt[0][in.getOperator().getConst<RecordSelect>().getField()].getSelector()), in[0]); } + TypeNode t = in.getType(); + // we only care about tuples and records here if(in.getKind() != kind::TUPLE && in.getKind() != kind::TUPLE_UPDATE && in.getKind() != kind::RECORD && in.getKind() != kind::RECORD_UPDATE) { + if((t.isTuple() || t.isRecord()) && in.hasAttribute(smt::BooleanTermAttr())) { + Debug("tuprec") << "should map " << in << " of type " << t << " back to " << in.getAttribute(smt::BooleanTermAttr()).getType() << endl; + Debug("tuprec") << "so " << NodeManager::currentNM()->getDatatypeForTupleRecord(t).getDatatype() << " goes to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getDatatype() << endl; + if(t.isTuple()) { + Debug("tuprec") << "current datatype-tuple-attr is " << NodeManager::currentNM()->getDatatypeForTupleRecord(t).getAttribute(expr::DatatypeTupleAttr()) << endl; + Debug("tuprec") << "setting to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeTupleAttr()) << endl; + NodeManager::currentNM()->getDatatypeForTupleRecord(t).setAttribute(expr::DatatypeTupleAttr(), NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeTupleAttr())); + } else { + Debug("tuprec") << "current datatype-record-attr is " << NodeManager::currentNM()->getDatatypeForTupleRecord(t).getAttribute(expr::DatatypeRecordAttr()) << endl; + Debug("tuprec") << "setting to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeRecordAttr()) << endl; + NodeManager::currentNM()->getDatatypeForTupleRecord(t).setAttribute(expr::DatatypeRecordAttr(), NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeRecordAttr())); + } + } // nothing to do return in; } - TypeNode t = in.getType(); - if(t.hasAttribute(expr::DatatypeTupleAttr())) { t = t.getAttribute(expr::DatatypeTupleAttr()); } else if(t.hasAttribute(expr::DatatypeRecordAttr())) { diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h index 2a74f6d15..a4facdefe 100644 --- a/src/theory/datatypes/type_enumerator.h +++ b/src/theory/datatypes/type_enumerator.h @@ -176,7 +176,7 @@ class TupleEnumerator : public TypeEnumeratorBase<TupleEnumerator> { void newEnumerators() { d_enumerators = new TypeEnumerator*[getType().getNumChildren()]; for(size_t i = 0; i < getType().getNumChildren(); ++i) { - d_enumerators[i] = NULL; + d_enumerators[i] = new TypeEnumerator(getType()[i]); } } @@ -205,9 +205,7 @@ public: if(te.d_enumerators != NULL) { newEnumerators(); for(size_t i = 0; i < getType().getNumChildren(); ++i) { - if(te.d_enumerators[i] != NULL) { - d_enumerators[i] = new TypeEnumerator(*te.d_enumerators[i]); - } + *d_enumerators[i] = TypeEnumerator(*te.d_enumerators[i]); } } } @@ -292,9 +290,7 @@ public: if(re.d_enumerators != NULL) { newEnumerators(); for(size_t i = 0; i < getType().getNumChildren(); ++i) { - if(re.d_enumerators[i] != NULL) { - d_enumerators[i] = new TypeEnumerator(*re.d_enumerators[i]); - } + *d_enumerators[i] = TypeEnumerator(*re.d_enumerators[i]); } } } diff --git a/src/theory/model.cpp b/src/theory/model.cpp index bbc51c9e0..42a5380e4 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -57,7 +57,7 @@ Node TheoryModel::getValue( TNode n ) const{ Expr TheoryModel::getValue( Expr expr ) const{ Node n = Node::fromExpr( expr ); Node ret = getValue( n ); - return d_smt.postprocess(ret).toExpr(); + return d_smt.postprocess(ret, TypeNode::fromType(expr.getType())).toExpr(); } /** get cardinality for sort */ diff --git a/src/theory/theory.h b/src/theory/theory.h index 5b2032430..94cf9accd 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -516,6 +516,11 @@ public: virtual EqualityStatus getEqualityStatus(TNode a, TNode b) { return EQUALITY_UNKNOWN; } /** + * Return the model value of the give shared term (or null if not avalilable. + */ + virtual Node getModelValue(TNode var) { return Node::null(); } + + /** * Check the current assignment's consistency. * * An implementation of check() is required to either: diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index f7f689850..b89ca8fa4 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1129,6 +1129,11 @@ theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) { return theoryOf(Theory::theoryOf(a.getType()))->getEqualityStatus(a, b); } +Node TheoryEngine::getModelValue(TNode var) { + Assert(d_sharedTerms.isShared(var)); + return theoryOf(Theory::theoryOf(var.getType()))->getModelValue(var); +} + static Node mkExplanation(const std::vector<NodeTheoryPair>& explanation) { std::set<TNode> all; diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index a3779f0e8..a8fe52498 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -709,6 +709,12 @@ public: */ theory::EqualityStatus getEqualityStatus(TNode a, TNode b); + /** + * Retruns the value that a theory that owns the type of var currently + * has (or null if none); + */ + Node getModelValue(TNode var); + private: /** Default visitor for pre-registration */ diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp index 389a17461..c5d2845bd 100644 --- a/src/theory/valuation.cpp +++ b/src/theory/valuation.cpp @@ -83,6 +83,11 @@ EqualityStatus Valuation::getEqualityStatus(TNode a, TNode b) { return d_engine->getEqualityStatus(a, b); } +Node Valuation::getModelValue(TNode var) { + return d_engine->getModelValue(var); +} + + Node Valuation::ensureLiteral(TNode n) { Debug("ensureLiteral") << "rewriting: " << n << std::endl; Node rewritten = Rewriter::rewrite(n); diff --git a/src/theory/valuation.h b/src/theory/valuation.h index f69bacc19..36e62a402 100644 --- a/src/theory/valuation.h +++ b/src/theory/valuation.h @@ -97,6 +97,11 @@ public: EqualityStatus getEqualityStatus(TNode a, TNode b); /** + * Returns the model value of the shared term (or null if not available). + */ + Node getModelValue(TNode var); + + /** * Ensure that the given node will have a designated SAT literal * that is definitionally equal to it. The result of this function * is a Node that can be queried via getSatValue(). |