diff options
Diffstat (limited to 'src')
75 files changed, 2276 insertions, 3873 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 9a1cfe9e7..7ecee2dee 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -124,6 +124,8 @@ libcvc4_add_sources( printer/tptp/tptp_printer.h proof/arith_proof.cpp proof/arith_proof.h + proof/arith_proof_recorder.cpp + proof/arith_proof_recorder.h proof/array_proof.cpp proof/array_proof.h proof/bitvector_proof.cpp @@ -142,6 +144,8 @@ libcvc4_add_sources( proof/proof_output_channel.h proof/proof_utils.cpp proof/proof_utils.h + proof/resolution_bitvector_proof.cpp + proof/resolution_bitvector_proof.h proof/sat_proof.h proof/sat_proof_implementation.h proof/simplify_boolean_node.cpp @@ -202,6 +206,7 @@ libcvc4_add_sources( prop/sat_solver.h prop/sat_solver_factory.cpp prop/sat_solver_factory.h + prop/bv_sat_solver_notify.h prop/sat_solver_types.h prop/theory_proxy.cpp prop/theory_proxy.h @@ -472,8 +477,6 @@ libcvc4_add_sources( theory/quantifiers/extended_rewrite.h theory/quantifiers/first_order_model.cpp theory/quantifiers/first_order_model.h - theory/quantifiers/fmf/ambqi_builder.cpp - theory/quantifiers/fmf/ambqi_builder.h theory/quantifiers/fmf/bounded_integers.cpp theory/quantifiers/fmf/bounded_integers.h theory/quantifiers/fmf/full_model_check.cpp diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index b4d3b013d..68b0301ec 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -635,6 +635,10 @@ class CVC4ApiExceptionStream CVC4_PREDICT_FALSE(cond) \ ? (void)0 : OstreamVoider() & CVC4ApiExceptionStream().ostream() +#define CVC4_API_CHECK_NOT_NULL \ + CVC4_API_CHECK(!isNull()) << "Invalid call to '" << __PRETTY_FUNCTION__ \ + << "', expected non-null object"; + #define CVC4_API_KIND_CHECK(kind) \ CVC4_API_CHECK(isDefinedKind(kind)) \ << "Invalid kind '" << kindToString(kind) << "'"; @@ -1166,9 +1170,17 @@ bool OpTerm::operator==(const OpTerm& t) const { return *d_expr == *t.d_expr; } bool OpTerm::operator!=(const OpTerm& t) const { return *d_expr != *t.d_expr; } -Kind OpTerm::getKind() const { return intToExtKind(d_expr->getKind()); } +Kind OpTerm::getKind() const +{ + CVC4_API_CHECK_NOT_NULL; + return intToExtKind(d_expr->getKind()); +} -Sort OpTerm::getSort() const { return Sort(d_expr->getType()); } +Sort OpTerm::getSort() const +{ + CVC4_API_CHECK_NOT_NULL; + return Sort(d_expr->getType()); +} bool OpTerm::isNull() const { return d_expr->isNull(); } @@ -1750,6 +1762,7 @@ Sort Solver::mkUninterpretedSort(const std::string& symbol) const Sort Solver::mkSortConstructorSort(const std::string& symbol, size_t arity) const { + CVC4_API_ARG_CHECK_EXPECTED(arity > 0, arity) << "an arity > 0"; return d_exprMgr->mkSortConstructor(symbol, arity); } diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt index c711567ab..b86db8d00 100644 --- a/src/options/CMakeLists.txt +++ b/src/options/CMakeLists.txt @@ -9,6 +9,8 @@ libcvc4_add_sources( arith_unate_lemma_mode.cpp arith_unate_lemma_mode.h base_handlers.h + bool_to_bv_mode.cpp + bool_to_bv_mode.h bv_bitblast_mode.cpp bv_bitblast_mode.h datatypes_modes.h diff --git a/src/options/bool_to_bv_mode.cpp b/src/options/bool_to_bv_mode.cpp new file mode 100644 index 000000000..670e15419 --- /dev/null +++ b/src/options/bool_to_bv_mode.cpp @@ -0,0 +1,42 @@ +/********************* */ +/*! \file bool_to_bv_mode.cpp +** \verbatim +** Top contributors (to current version): +** Makai Mann +** This file is part of the CVC4 project. +** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS +** in the top-level source directory) and their institutional affiliations. +** All rights reserved. See the file COPYING in the top-level source +** directory for licensing information.\endverbatim +** +** \brief Modes for bool-to-bv preprocessing pass +** +** Modes for bool-to-bv preprocessing pass which tries to lower booleans +** to bit-vectors of width 1 at various levels of aggressiveness. +**/ + +#include "options/bool_to_bv_mode.h" + +#include <iostream> + + +namespace CVC4 +{ + std::ostream& operator<<(std::ostream& out, preprocessing::passes::BoolToBVMode mode) { + switch(mode) { + case preprocessing::passes::BOOL_TO_BV_OFF: + out << "BOOL_TO_BV_OFF"; + break; + case preprocessing::passes::BOOL_TO_BV_ITE: + out << "BOOL_TO_BV_ITE"; + break; + case preprocessing::passes::BOOL_TO_BV_ALL: + out << "BOOL_TO_BV_ALL"; + break; + default: + out << "BoolToBVMode:UNKNOWN![" << unsigned(mode) << "]"; + } + + return out; + } +} // namespace CVC4 diff --git a/src/options/bool_to_bv_mode.h b/src/options/bool_to_bv_mode.h new file mode 100644 index 000000000..f2911c339 --- /dev/null +++ b/src/options/bool_to_bv_mode.h @@ -0,0 +1,57 @@ +/********************* */ +/*! \file bool_to_bv_mode.h +** \verbatim +** Top contributors (to current version): +** Makai Mann +** This file is part of the CVC4 project. +** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS +** in the top-level source directory) and their institutional affiliations. +** All rights reserved. See the file COPYING in the top-level source +** directory for licensing information.\endverbatim +** +** \brief Modes for bool-to-bv preprocessing pass +** +** Modes for bool-to-bv preprocessing pass which tries to lower booleans +** to bit-vectors of width 1 at various levels of aggressiveness. +**/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_MODE_H +#define __CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_MODE_H + +#include <iosfwd> + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +/** Enumeration of bool-to-bv modes */ +enum BoolToBVMode +{ + /** + * No bool-to-bv pass + */ + BOOL_TO_BV_OFF, + + /** + * Only lower bools in condition of ITEs + * Tries to give more info to bit-vector solver + * by using bit-vector-ITEs when possible + */ + BOOL_TO_BV_ITE, + + /** + * Lower every bool beneath the top layer to be a + * bit-vector + */ + BOOL_TO_BV_ALL +}; +} +} + +std::ostream& operator<<(std::ostream& out, preprocessing::passes::BoolToBVMode mode); + +} + +#endif /* __CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_MODE_H */ diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml index 15a9047c7..00290da7d 100644 --- a/src/options/bv_options.toml +++ b/src/options/bv_options.toml @@ -105,11 +105,22 @@ header = "options/bv_options.h" [[option]] name = "boolToBitvector" + smt_name = "bool-to-bv" category = "regular" - long = "bool-to-bv" + long = "bool-to-bv=MODE" + type = "CVC4::preprocessing::passes::BoolToBVMode" + default = "CVC4::preprocessing::passes::BOOL_TO_BV_OFF" + handler = "stringToBoolToBVMode" + includes = ["options/bool_to_bv_mode.h"] + help = "convert booleans to bit-vectors of size 1 at various levels of aggressiveness, see --bool-to-bv=help" + +[[option]] + name = "bitwiseEq" + category = "regular" + long = "bitwise-eq" type = "bool" - default = "false" - help = "convert booleans to bit-vectors of size 1 when possible" + default = "true" + help = "lift equivalence with one-bit bit-vectors to be boolean operations" [[option]] name = "bitvectorDivByZeroConst" diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index bd5b00728..36144e70e 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -267,7 +267,8 @@ agg \n\ \n\ "; -const std::string OptionsHandler::s_mbqiModeHelp = "\ +const std::string OptionsHandler::s_mbqiModeHelp = + "\ Model-based quantifier instantiation modes currently supported by the --mbqi option:\n\ \n\ default \n\ @@ -277,12 +278,8 @@ default \n\ none \n\ + Disable model-based quantifier instantiation.\n\ \n\ -gen-ev \n\ -+ Use model-based quantifier instantiation algorithm from CADE 24 finite\n\ - model finding paper based on generalizing evaluations.\n\ -\n\ -abs \n\ -+ Use abstract MBQI algorithm (uses disjoint sets). \n\ +trust \n\ ++ Do not instantiate quantified formulas (incomplete technique).\n\ \n\ "; @@ -660,14 +657,11 @@ void OptionsHandler::checkLiteralMatchMode( theory::quantifiers::MbqiMode OptionsHandler::stringToMbqiMode( std::string option, std::string optarg) { - if(optarg == "gen-ev") { - return theory::quantifiers::MBQI_GEN_EVAL; - } else if(optarg == "none") { + if (optarg == "none") + { return theory::quantifiers::MBQI_NONE; } else if(optarg == "default" || optarg == "fmc") { return theory::quantifiers::MBQI_FMC; - } else if(optarg == "abs") { - return theory::quantifiers::MBQI_ABS; } else if(optarg == "trust") { return theory::quantifiers::MBQI_TRUST; } else if(optarg == "help") { @@ -1301,6 +1295,50 @@ theory::bv::BvSlicerMode OptionsHandler::stringToBvSlicerMode( } } +const std::string OptionsHandler::s_boolToBVModeHelp = + "\ +BoolToBV pass modes supported by the --bool-to-bv option:\n\ +\n\ +off (default)\n\ ++ Don't push any booleans to width one bit-vectors\n\ +\n\ +ite\n\ ++ Try to turn ITEs into BITVECTOR_ITE when possible. It can fail per-formula \n\ + if not all sub-formulas can be turned to bit-vectors\n\ +\n\ +all\n\ ++ Force all booleans to be bit-vectors of width one except at the top level.\n\ + Most aggressive mode\n\ +"; + +preprocessing::passes::BoolToBVMode OptionsHandler::stringToBoolToBVMode( + std::string option, std::string optarg) +{ + if (optarg == "off") + { + return preprocessing::passes::BOOL_TO_BV_OFF; + } + else if (optarg == "ite") + { + return preprocessing::passes::BOOL_TO_BV_ITE; + } + else if (optarg == "all") + { + return preprocessing::passes::BOOL_TO_BV_ALL; + } + else if (optarg == "help") + { + puts(s_boolToBVModeHelp.c_str()); + exit(1); + } + else + { + throw OptionException(std::string("unknown option for --bool-to-bv: `") + + optarg + + "'. Try --bool-to-bv=help"); + } +} + void OptionsHandler::setBitblastAig(std::string option, bool arg) { if(arg) { @@ -1632,7 +1670,14 @@ void OptionsHandler::setProduceAssertions(std::string option, bool value) void OptionsHandler::proofEnabledBuild(std::string option, bool value) { -#ifndef CVC4_PROOF +#ifdef CVC4_PROOF + if (value && options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER + && options::bvSatSolver() != theory::bv::SAT_SOLVER_MINISAT) + { + throw OptionException( + "Eager BV proofs only supported when minisat is used"); + } +#else if(value) { std::stringstream ss; ss << "option `" << option << "' requires a proofs-enabled build of CVC4; this binary was not built with proof support"; diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 53e317895..f96632696 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -27,6 +27,7 @@ #include "options/arith_propagation_mode.h" #include "options/arith_unate_lemma_mode.h" #include "options/base_handlers.h" +#include "options/bool_to_bv_mode.h" #include "options/bv_bitblast_mode.h" #include "options/datatypes_modes.h" #include "options/decision_mode.h" @@ -137,6 +138,8 @@ public: std::string optarg); theory::bv::BvSlicerMode stringToBvSlicerMode(std::string option, std::string optarg); + preprocessing::passes::BoolToBVMode stringToBoolToBVMode(std::string option, + std::string optarg); void setBitblastAig(std::string option, bool arg); theory::bv::SatSolverMode stringToSatSolver(std::string option, @@ -229,6 +232,7 @@ public: static const std::string s_bvSatSolverHelp; static const std::string s_booleanTermConversionModeHelp; static const std::string s_bvSlicerModeHelp; + static const std::string s_boolToBVModeHelp; static const std::string s_cegqiFairModeHelp; static const std::string s_decisionModeHelp; static const std::string s_instFormatHelp ; diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index 85a9747fe..9650aba7a 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -112,7 +112,7 @@ struct OptionHandler<T, true, true> { if(!success){ throw OptionException(option + ": failed to parse "+ optionarg + - " as an integer of the appropraite type."); + " as an integer of the appropriate type."); } // Depending in the platform unsigned numbers with '-' signs may parse. diff --git a/src/options/quantifiers_modes.cpp b/src/options/quantifiers_modes.cpp index 1814a363d..b08f71c2e 100644 --- a/src/options/quantifiers_modes.cpp +++ b/src/options/quantifiers_modes.cpp @@ -64,18 +64,12 @@ std::ostream& operator<<(std::ostream& out, theory::quantifiers::LiteralMatchMod std::ostream& operator<<(std::ostream& out, theory::quantifiers::MbqiMode mode) { switch(mode) { - case theory::quantifiers::MBQI_GEN_EVAL: - out << "MBQI_GEN_EVAL"; - break; case theory::quantifiers::MBQI_NONE: out << "MBQI_NONE"; break; case theory::quantifiers::MBQI_FMC: out << "MBQI_FMC"; break; - case theory::quantifiers::MBQI_ABS: - out << "MBQI_ABS"; - break; case theory::quantifiers::MBQI_TRUST: out << "MBQI_TRUST"; break; diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h index 41378d2cd..eea043865 100644 --- a/src/options/quantifiers_modes.h +++ b/src/options/quantifiers_modes.h @@ -53,14 +53,10 @@ enum LiteralMatchMode { }; enum MbqiMode { - /** mbqi from CADE 24 paper */ - MBQI_GEN_EVAL, /** no mbqi */ MBQI_NONE, /** default, mbqi from Section 5.4.2 of AJR thesis */ MBQI_FMC, - /** abstract mbqi algorithm */ - MBQI_ABS, /** mbqi trust (produce no instantiations) */ MBQI_TRUST, }; diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml index 77056e279..3544c37fe 100644 --- a/src/options/strings_options.toml +++ b/src/options/strings_options.toml @@ -205,7 +205,7 @@ header = "options/strings_options.h" category = "regular" long = "re-elim" type = "bool" - default = "false" + default = "true" help = "elimination techniques for regular expressions" [[option]] diff --git a/src/preprocessing/passes/bool_to_bv.cpp b/src/preprocessing/passes/bool_to_bv.cpp index c8a59bdc4..252ab941c 100644 --- a/src/preprocessing/passes/bool_to_bv.cpp +++ b/src/preprocessing/passes/bool_to_bv.cpp @@ -9,17 +9,17 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief The BoolToBv preprocessing pass + ** \brief The BoolToBV preprocessing pass ** **/ #include "preprocessing/passes/bool_to_bv.h" #include <string> -#include <unordered_map> -#include <vector> +#include "base/map_util.h" #include "expr/node.h" +#include "options/bv_options.h" #include "smt/smt_statistics_registry.h" #include "theory/rewriter.h" #include "theory/theory.h" @@ -30,183 +30,253 @@ namespace passes { using namespace CVC4::theory; BoolToBV::BoolToBV(PreprocessingPassContext* preprocContext) - : PreprocessingPass(preprocContext, "bool-to-bv"), - d_lowerCache(), - d_one(bv::utils::mkOne(1)), - d_zero(bv::utils::mkZero(1)), - d_statistics(){}; + : PreprocessingPass(preprocContext, "bool-to-bv"), d_statistics(){}; PreprocessingPassResult BoolToBV::applyInternal( AssertionPipeline* assertionsToPreprocess) { NodeManager::currentResourceManager()->spendResource( options::preprocessStep()); - std::vector<Node> new_assertions; - lowerBoolToBv(assertionsToPreprocess->ref(), new_assertions); - for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i) + + unsigned size = assertionsToPreprocess->size(); + for (unsigned i = 0; i < size; ++i) { - assertionsToPreprocess->replace(i, Rewriter::rewrite(new_assertions[i])); + assertionsToPreprocess->replace( + i, Rewriter::rewrite(lowerAssertion((*assertionsToPreprocess)[i]))); } - return PreprocessingPassResult::NO_CONFLICT; -} -void BoolToBV::addToLowerCache(TNode term, Node new_term) -{ - Assert(new_term != Node()); - Assert(!hasLowerCache(term)); - d_lowerCache[term] = new_term; + return PreprocessingPassResult::NO_CONFLICT; } -Node BoolToBV::getLowerCache(TNode term) const +Node BoolToBV::fromCache(TNode n) const { - Assert(hasLowerCache(term)); - return d_lowerCache.find(term)->second; + if (d_lowerCache.find(n) != d_lowerCache.end()) + { + return d_lowerCache.find(n)->second; + } + return n; } -bool BoolToBV::hasLowerCache(TNode term) const +bool BoolToBV::needToRebuild(TNode n) const { - return d_lowerCache.find(term) != d_lowerCache.end(); + // check if any children were rebuilt + for (const Node& nn : n) + { + if (ContainsKey(d_lowerCache, nn)) + { + return true; + } + } + return false; } -Node BoolToBV::lowerNode(TNode current, bool topLevel) +Node BoolToBV::lowerAssertion(const TNode& a) { - Node result; + bool optionITE = options::boolToBitvector() == BOOL_TO_BV_ITE; NodeManager* nm = NodeManager::currentNM(); - if (hasLowerCache(current)) - { - result = getLowerCache(current); - } - else + std::vector<TNode> visit; + visit.push_back(a); + std::unordered_set<TNode, TNodeHashFunction> visited; + // for ite mode, keeps track of whether you're in an ite condition + // for all mode, unused + std::unordered_set<TNode, TNodeHashFunction> ite_cond; + + while (!visit.empty()) { - if (current.getNumChildren() == 0) + TNode n = visit.back(); + visit.pop_back(); + + int numChildren = n.getNumChildren(); + Kind k = n.getKind(); + Debug("bool-to-bv") << "BoolToBV::lowerAssertion Post-traversal with " << n + << " and visited = " << ContainsKey(visited, n) + << std::endl; + + // Mark as visited + /* Optimization: if it's a leaf, don't need to wait to do the work */ + if (!ContainsKey(visited, n) && (numChildren > 0)) { - if (current.getKind() == kind::CONST_BOOLEAN) + visited.insert(n); + visit.push_back(n); + + // insert children in reverse order so that they're processed in order + // important for rewriting which sorts by node id + for (int i = numChildren - 1; i >= 0; --i) { - result = (current == bv::utils::mkTrue()) ? d_one : d_zero; + visit.push_back(n[i]); } - else + + if (optionITE) { - result = current; + // check for ite-conditions + if (k == kind::ITE) + { + ite_cond.insert(n[0]); + } + else if (ContainsKey(ite_cond, n)) + { + // being part of an ite condition is inherited from the parent + ite_cond.insert(n.begin(), n.end()); + } } } + /* Optimization for ite mode */ + else if (optionITE && !ContainsKey(ite_cond, n) && !needToRebuild(n)) + { + Debug("bool-to-bv") + << "BoolToBV::lowerAssertion Skipping because don't need to rebuild: " + << n << std::endl; + // in ite mode, if you've already visited the node but it's not + // in an ite condition and doesn't need to be rebuilt, then + // don't need to do anything + continue; + } else { - Kind kind = current.getKind(); - Kind new_kind = kind; - switch (kind) - { - case kind::EQUAL: - if (current[0].getType().isBitVector() - || current[0].getType().isBoolean()) - { - new_kind = kind::BITVECTOR_COMP; - } - break; - case kind::AND: new_kind = kind::BITVECTOR_AND; break; - case kind::OR: new_kind = kind::BITVECTOR_OR; break; - case kind::NOT: new_kind = kind::BITVECTOR_NOT; break; - case kind::XOR: new_kind = kind::BITVECTOR_XOR; break; - case kind::IMPLIES: new_kind = kind::BITVECTOR_OR; break; - case kind::ITE: - if (current.getType().isBitVector() || current.getType().isBoolean()) - { - new_kind = kind::BITVECTOR_ITE; - } - break; - case kind::BITVECTOR_ULT: new_kind = kind::BITVECTOR_ULTBV; break; - case kind::BITVECTOR_SLT: new_kind = kind::BITVECTOR_SLTBV; break; - case kind::BITVECTOR_ULE: - case kind::BITVECTOR_UGT: - case kind::BITVECTOR_UGE: - case kind::BITVECTOR_SLE: - case kind::BITVECTOR_SGT: - case kind::BITVECTOR_SGE: - // Should have been removed by rewriting. - Unreachable(); - default: break; - } - NodeBuilder<> builder(new_kind); - if (kind != new_kind) - { - ++(d_statistics.d_numTermsLowered); - } - if (current.getMetaKind() == kind::metakind::PARAMETERIZED) - { - builder << current.getOperator(); - } - Node converted; - if (new_kind == kind::ITE) + lowerNode(n); + } + } + + if (fromCache(a).getType().isBitVector()) + { + return nm->mkNode(kind::EQUAL, fromCache(a), bv::utils::mkOne(1)); + } + else + { + Assert(a == fromCache(a)); + return a; + } +} + +void BoolToBV::lowerNode(const TNode& n) +{ + NodeManager* nm = NodeManager::currentNM(); + Kind k = n.getKind(); + + bool all_bv = true; + // check if it was able to convert all children to bitvectors + for (const Node& nn : n) + { + all_bv = all_bv && fromCache(nn).getType().isBitVector(); + if (!all_bv) + { + break; + } + } + + if (!all_bv || (n.getNumChildren() == 0)) + { + if ((options::boolToBitvector() == BOOL_TO_BV_ALL) + && n.getType().isBoolean()) + { + if (k == kind::CONST_BOOLEAN) { - // Special-case ITE because need condition to be Boolean. - converted = lowerNode(current[0], true); - builder << converted; - converted = lowerNode(current[1]); - builder << converted; - converted = lowerNode(current[2]); - builder << converted; - } - else if (kind == kind::IMPLIES) { - // Special-case IMPLIES because needs to be rewritten. - converted = lowerNode(current[0]); - builder << nm->mkNode(kind::BITVECTOR_NOT, converted); - converted = lowerNode(current[1]); - builder << converted; + d_lowerCache[n] = (n == bv::utils::mkTrue()) ? bv::utils::mkOne(1) + : bv::utils::mkZero(1); } else { - for (unsigned i = 0; i < current.getNumChildren(); ++i) - { - converted = lowerNode(current[i]); - builder << converted; - } + d_lowerCache[n] = + nm->mkNode(kind::ITE, n, bv::utils::mkOne(1), bv::utils::mkZero(1)); } - result = builder; + + Debug("bool-to-bv") << "BoolToBV::lowerNode " << n << " =>\n" + << fromCache(n) << std::endl; + ++(d_statistics.d_numTermsForcedLowered); + return; } - if (result.getType().isBoolean()) + else { - ++(d_statistics.d_numTermsForcedLowered); - result = nm->mkNode(kind::ITE, result, d_one, d_zero); + // invariant + // either one of the children is not a bit-vector or bool + // i.e. something that can't be 'forced' to a bitvector + // or it's in 'ite' mode which will give up on bools that + // can't be converted easily + + Debug("bool-to-bv") << "BoolToBV::lowerNode skipping: " << n << std::endl; + return; } - addToLowerCache(current, result); } - if (topLevel) + + Kind new_kind = k; + switch (k) { - result = nm->mkNode(kind::EQUAL, result, d_one); + case kind::EQUAL: new_kind = kind::BITVECTOR_COMP; break; + case kind::AND: new_kind = kind::BITVECTOR_AND; break; + case kind::OR: new_kind = kind::BITVECTOR_OR; break; + case kind::NOT: new_kind = kind::BITVECTOR_NOT; break; + case kind::XOR: new_kind = kind::BITVECTOR_XOR; break; + case kind::IMPLIES: new_kind = kind::BITVECTOR_OR; break; + case kind::ITE: new_kind = kind::BITVECTOR_ITE; break; + case kind::BITVECTOR_ULT: new_kind = kind::BITVECTOR_ULTBV; break; + case kind::BITVECTOR_SLT: new_kind = kind::BITVECTOR_SLTBV; break; + case kind::BITVECTOR_ULE: + case kind::BITVECTOR_UGT: + case kind::BITVECTOR_UGE: + case kind::BITVECTOR_SLE: + case kind::BITVECTOR_SGT: + case kind::BITVECTOR_SGE: + // Should have been removed by rewriting. + Unreachable(); + default: break; } - Assert(result != Node()); - Debug("bool-to-bv") << "BoolToBV::lowerNode " << current << " => \n" - << result << "\n"; - return result; -} -void BoolToBV::lowerBoolToBv(const std::vector<Node>& assertions, - std::vector<Node>& new_assertions) -{ - for (unsigned i = 0; i < assertions.size(); ++i) + NodeBuilder<> builder(new_kind); + if ((options::boolToBitvector() == BOOL_TO_BV_ALL) && (new_kind != k)) + { + ++(d_statistics.d_numTermsLowered); + } + + if (n.getMetaKind() == kind::metakind::PARAMETERIZED) + { + builder << n.getOperator(); + } + + // special case IMPLIES because needs to be rewritten + if (k == kind::IMPLIES) + { + builder << nm->mkNode(kind::BITVECTOR_NOT, fromCache(n[0])); + builder << fromCache(n[1]); + } + else { - Node new_assertion = lowerNode(assertions[i], true); - new_assertions.push_back(new_assertion); - Trace("bool-to-bv") << " " << assertions[i] << " => " << new_assertions[i] - << "\n"; + for (const Node& nn : n) + { + builder << fromCache(nn); + } } + + Debug("bool-to-bv") << "BoolToBV::lowerNode " << n << " =>\n" + << builder << std::endl; + + d_lowerCache[n] = builder.constructNode(); } BoolToBV::Statistics::Statistics() - : d_numTermsLowered("preprocessing::passes::BoolToBV::NumTermsLowered", 0), - d_numAtomsLowered("preprocessing::passes::BoolToBV::NumAtomsLowered", 0), + : d_numIteToBvite("preprocessing::passes::BoolToBV::NumIteToBvite", 0), + d_numTermsLowered("preprocessing::passes:BoolToBV::NumTermsLowered", 0), d_numTermsForcedLowered( "preprocessing::passes::BoolToBV::NumTermsForcedLowered", 0) { - smtStatisticsRegistry()->registerStat(&d_numTermsLowered); - smtStatisticsRegistry()->registerStat(&d_numAtomsLowered); - smtStatisticsRegistry()->registerStat(&d_numTermsForcedLowered); + smtStatisticsRegistry()->registerStat(&d_numIteToBvite); + if (options::boolToBitvector() == BOOL_TO_BV_ALL) + { + // these statistics wouldn't be correct in the ITE mode, + // because it might discard rebuilt nodes if it fails to + // convert a bool to width-one bit-vector (never forces) + smtStatisticsRegistry()->registerStat(&d_numTermsLowered); + smtStatisticsRegistry()->registerStat(&d_numTermsForcedLowered); + } } BoolToBV::Statistics::~Statistics() { - smtStatisticsRegistry()->unregisterStat(&d_numTermsLowered); - smtStatisticsRegistry()->unregisterStat(&d_numAtomsLowered); - smtStatisticsRegistry()->unregisterStat(&d_numTermsForcedLowered); + smtStatisticsRegistry()->unregisterStat(&d_numIteToBvite); + if (options::boolToBitvector() == BOOL_TO_BV_ALL) + { + smtStatisticsRegistry()->unregisterStat(&d_numTermsLowered); + smtStatisticsRegistry()->unregisterStat(&d_numTermsForcedLowered); + } } diff --git a/src/preprocessing/passes/bool_to_bv.h b/src/preprocessing/passes/bool_to_bv.h index 49c9dc944..da99d3c84 100644 --- a/src/preprocessing/passes/bool_to_bv.h +++ b/src/preprocessing/passes/bool_to_bv.h @@ -2,14 +2,14 @@ /*! \file bool_to_bv.h ** \verbatim ** Top contributors (to current version): - ** Yoni Zohar + ** Makai Mann, Yoni Zohar ** This file is part of the CVC4 project. ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief The BoolToBv preprocessing pass + ** \brief The BoolToBV preprocessing pass ** **/ @@ -18,9 +18,9 @@ #ifndef __CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H #define __CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H -#include "preprocessing/passes/bv_to_bool.h" #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" +#include "theory/bv/theory_bv_utils.h" #include "util/statistics_registry.h" namespace CVC4 { @@ -39,24 +39,33 @@ class BoolToBV : public PreprocessingPass private: struct Statistics { + IntStat d_numIteToBvite; IntStat d_numTermsLowered; - IntStat d_numAtomsLowered; IntStat d_numTermsForcedLowered; Statistics(); ~Statistics(); }; - void lowerBoolToBv(const std::vector<Node>& assertions, - std::vector<Node>& new_assertions); - void addToLowerCache(TNode term, Node new_term); - Node getLowerCache(TNode term) const; - bool hasLowerCache(TNode term) const; - Node lowerNode(TNode current, bool topLevel = false); - NodeNodeMap d_lowerCache; - Node d_one; - Node d_zero; + /* Takes an assertion and tries to create more bit-vector structure */ + Node lowerAssertion(const TNode& a); + + /* Tries to lower one node to a width-one bit-vector */ + void lowerNode(const TNode& n); + + /* Returns cached node if it exists, otherwise returns the node */ + Node fromCache(TNode n) const; + + /** Checks if any of the nodes children were rebuilt, + * in which case n needs to be rebuilt as well + */ + bool needToRebuild(TNode n) const; + Statistics d_statistics; -}; // class + + /* Keeps track of lowered nodes */ + std::unordered_map<Node, Node, NodeHashFunction> d_lowerCache; +}; // class BoolToBV + } // namespace passes } // namespace preprocessing } // namespace CVC4 diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp index 3b57be1f2..1d51f99e1 100644 --- a/src/proof/arith_proof.cpp +++ b/src/proof/arith_proof.cpp @@ -640,8 +640,10 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, } ArithProof::ArithProof(theory::arith::TheoryArith* arith, TheoryProofEngine* pe) - : TheoryProof(arith, pe), d_realMode(false) -{} + : TheoryProof(arith, pe), d_recorder(), d_realMode(false) +{ + arith->setProofRecorder(&d_recorder); +} theory::TheoryId ArithProof::getTheoryId() { return theory::THEORY_ARITH; } void ArithProof::registerTerm(Expr term) { diff --git a/src/proof/arith_proof.h b/src/proof/arith_proof.h index 27012184a..a58294998 100644 --- a/src/proof/arith_proof.h +++ b/src/proof/arith_proof.h @@ -23,6 +23,7 @@ #include <unordered_set> #include "expr/expr.h" +#include "proof/arith_proof_recorder.h" #include "proof/proof_manager.h" #include "proof/theory_proof.h" #include "theory/uf/equality_engine.h" @@ -62,6 +63,11 @@ protected: // TypeSet d_sorts; // all the uninterpreted sorts in this theory ExprSet d_declarations; // all the variable/function declarations + /** + * @brief Where farkas proofs of lemmas are stored. + */ + proof::ArithProofRecorder d_recorder; + bool d_realMode; theory::TheoryId getTheoryId() override; diff --git a/src/proof/arith_proof_recorder.cpp b/src/proof/arith_proof_recorder.cpp new file mode 100644 index 000000000..d654ea073 --- /dev/null +++ b/src/proof/arith_proof_recorder.cpp @@ -0,0 +1,81 @@ +/********************* */ +/*! \file arith_proof_recorder.cpp + ** \verbatim + ** Top contributors (to current version): + ** Alex Ozdemir + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief A class for recording the skeletons of arithmetic proofs at solve + ** time so they can later be used during proof-production time. + **/ + +#include "proof/arith_proof_recorder.h" + +#include <algorithm> +#include <vector> + +#include "base/map_util.h" + +namespace CVC4 { +namespace proof { + +ArithProofRecorder::ArithProofRecorder() : d_lemmasToFarkasCoefficients() +{ + // Nothing else +} +void ArithProofRecorder::saveFarkasCoefficients( + Node conflict, theory::arith::RationalVectorCP farkasCoefficients) +{ + Assert(conflict.getKind() == kind::AND); + Assert(conflict.getNumChildren() == farkasCoefficients->size()); + for (size_t i = 0; i < conflict.getNumChildren(); ++i) + { + const Node& child = conflict[i]; + Assert(child.getType().isBoolean() && child[0].getType().isReal()); + } + Debug("pf::arith") << "Saved Farkas Coefficients:" << std::endl; + if (Debug.isOn("pf::arith")) + { + for (size_t i = 0; i < conflict.getNumChildren(); ++i) + { + const Node& child = conflict[i]; + const Rational& r = (*farkasCoefficients)[i]; + Debug("pf::arith") << " " << std::setw(8) << r; + Debug("pf::arith") << " " << child << std::endl; + } + } + + std::set<Node> lits; + std::copy( + conflict.begin(), conflict.end(), std::inserter(lits, lits.begin())); + + d_lemmasToFarkasCoefficients[lits] = + std::make_pair(std::move(conflict), *farkasCoefficients); +} + +bool ArithProofRecorder::hasFarkasCoefficients( + const std::set<Node>& conflict) const +{ + return d_lemmasToFarkasCoefficients.find(conflict) + != d_lemmasToFarkasCoefficients.end(); +} + +std::pair<Node, theory::arith::RationalVectorCP> +ArithProofRecorder::getFarkasCoefficients(const std::set<Node>& conflict) const +{ + if (auto *p = FindOrNull(d_lemmasToFarkasCoefficients, conflict)) + { + return std::make_pair(p->first, &p->second); + } + else + { + return std::make_pair(Node(), theory::arith::RationalVectorCPSentinel); + } +} + +} // namespace proof +} // namespace CVC4 diff --git a/src/proof/arith_proof_recorder.h b/src/proof/arith_proof_recorder.h new file mode 100644 index 000000000..2d0501332 --- /dev/null +++ b/src/proof/arith_proof_recorder.h @@ -0,0 +1,107 @@ +/********************* */ +/*! \file arith_proof_recorder.h + ** \verbatim + ** Top contributors (to current version): + ** Alex Ozdemir + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief A class for recording the skeletons of arithmetic proofs at solve + ** time so they can later be used during proof-production time. + ** + ** In particular, we're interested in proving bottom from a conjunction of + ** theory literals. + ** + ** For now, we assume that this can be done using a Farkas combination, and if + ** that doesn't work for some reason, then we give up and "trust" the lemma. + ** In the future we'll build support for more sophisticated reasoning. + ** + ** Given this scope, our task is to... + ** for each lemma (a set of literals) + ** save the Farkas coefficients for those literals + ** which requires we save an ordering of the literals + ** and a parallel ordering of Farkas coefficients. + ** + ** Farkas proofs have the following core structure: + ** For a list of affine bounds: c[i] dot x >= b[i] + ** (x is a vector of variables) + ** (c[i] is a vector of coefficients) + ** and a list of non-negative coefficients: f[i], + ** compute + ** + ** sum_i{ (c[i] dot x) * f[i] } and sum_i{b[i]*f[i]} + ** + ** and then verify that the left is actually < the right, a contradiction + ** + ** To be clear: this code does not check Farkas proofs, it just stores the + ** information needed to write them. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PROOF__ARITH_PROOF_RECORDER_H +#define __CVC4__PROOF__ARITH_PROOF_RECORDER_H + +#include <map> +#include <set> + +#include "expr/node.h" +#include "theory/arith/constraint_forward.h" + +namespace CVC4 { +namespace proof { + +class ArithProofRecorder +{ + public: + ArithProofRecorder(); + + /** + * @brief For a set of incompatible literals, save the Farkas coefficients + * demonstrating their incompatibility + * + * @param conflict a conjunction of conflicting literals + * @param farkasCoefficients a list of rational coefficients which the literals + * should be multiplied by (pairwise) to produce a contradiction. + * + * The orders of the two vectors must agree! + */ + void saveFarkasCoefficients( + Node conflict, theory::arith::RationalVectorCP farkasCoefficients); + + /** + * @brief Determine whether some literals have a Farkas proof of their + * incompatibility + * + * @param conflict a conjunction of (putatively) conflicting literals + * + * @return whether or not there is actually a proof for them. + */ + bool hasFarkasCoefficients(const std::set<Node>& conflict) const; + + /** + * @brief Get the Farkas Coefficients object + * + * @param conflict a conjunction of conflicting literals + * @return theory::arith::RationalVectorCP -- the Farkas coefficients + * Node -- a conjunction of the problem literals in coefficient order + * + * theory::arith::RationalVectorCPSentinel if there is no entry for + * these lits + */ + std::pair<Node, theory::arith::RationalVectorCP> getFarkasCoefficients( + const std::set<Node>& conflict) const; + + protected: + // For each lemma, save the Farkas coefficients of that lemma + std::map<std::set<Node>, std::pair<Node, theory::arith::RationalVector>> + d_lemmasToFarkasCoefficients; +}; + +} // namespace proof +} // namespace CVC4 + +#endif diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp index 8f001ffa1..9eb39e2e2 100644 --- a/src/proof/bitvector_proof.cpp +++ b/src/proof/bitvector_proof.cpp @@ -9,31 +9,19 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** [[ Add lengthier description here ]] - - ** \todo document this file - -**/ + ** Contains implementions (e.g. code for printing bitblasting bindings that is + ** common to all kinds of bitvector proofs. + **/ #include "proof/bitvector_proof.h" #include "options/bv_options.h" #include "options/proof_options.h" -#include "proof/array_proof.h" -#include "proof/clause_id.h" -#include "proof/lfsc_proof_printer.h" #include "proof/proof_output_channel.h" -#include "proof/proof_utils.h" -#include "proof/sat_proof_implementation.h" -#include "prop/bvminisat/bvminisat.h" +#include "proof/theory_proof.h" #include "theory/bv/bitblast/bitblaster.h" #include "theory/bv/theory_bv.h" -#include "theory/bv/theory_bv_rewrite_rules.h" - -using namespace CVC4::theory; -using namespace CVC4::theory::bv; namespace CVC4 { - BitVectorProof::BitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine) : TheoryProof(bv, proofEngine), @@ -41,73 +29,44 @@ BitVectorProof::BitVectorProof(theory::bv::TheoryBV* bv, d_seenBBTerms(), d_bbTerms(), d_bbAtoms(), - d_resolutionProof(NULL), - d_cnfProof(NULL), - d_isAssumptionConflict(false), - d_bitblaster(NULL), - d_useConstantLetification(false) {} - -void BitVectorProof::initSatProof(CVC4::BVMinisat::Solver* solver) { - Assert (d_resolutionProof == NULL); - d_resolutionProof = new BVSatProof(solver, &d_fakeContext, "bb", true); -} - -theory::TheoryId BitVectorProof::getTheoryId() { return theory::THEORY_BV; } -void BitVectorProof::initCnfProof(prop::CnfStream* cnfStream, - context::Context* cnf) { - Assert (d_resolutionProof != NULL); - Assert (d_cnfProof == NULL); - d_cnfProof = new LFSCCnfProof(cnfStream, cnf, "bb"); - - // true and false have to be setup in a special way - Node true_node = NodeManager::currentNM()->mkConst<bool>(true); - Node false_node = NodeManager::currentNM()->mkConst<bool>(false).notNode(); - - d_cnfProof->pushCurrentAssertion(true_node); - d_cnfProof->pushCurrentDefinition(true_node); - d_cnfProof->registerConvertedClause(d_resolutionProof->getTrueUnit()); - d_cnfProof->popCurrentAssertion(); - d_cnfProof->popCurrentDefinition(); - - d_cnfProof->pushCurrentAssertion(false_node); - d_cnfProof->pushCurrentDefinition(false_node); - d_cnfProof->registerConvertedClause(d_resolutionProof->getFalseUnit()); - d_cnfProof->popCurrentAssertion(); - d_cnfProof->popCurrentDefinition(); + d_bitblaster(nullptr), + d_useConstantLetification(false), + d_cnfProof() +{ } -void BitVectorProof::setBitblaster(bv::TBitblaster<Node>* bb) { - Assert (d_bitblaster == NULL); +void BitVectorProof::setBitblaster(theory::bv::TBitblaster<Node>* bb) +{ + Assert(d_bitblaster == NULL); d_bitblaster = bb; } -BVSatProof* BitVectorProof::getSatProof() { - Assert (d_resolutionProof != NULL); - return d_resolutionProof; -} - -void BitVectorProof::registerTermBB(Expr term) { - Debug("pf::bv") << "BitVectorProof::registerTermBB( " << term << " )" << std::endl; +void BitVectorProof::registerTermBB(Expr term) +{ + Debug("pf::bv") << "BitVectorProof::registerTermBB( " << term + << " )" << std::endl; - if (d_seenBBTerms.find(term) != d_seenBBTerms.end()) - return; + if (d_seenBBTerms.find(term) != d_seenBBTerms.end()) return; d_seenBBTerms.insert(term); d_bbTerms.push_back(term); - // If this term gets used in the final proof, we will want to register it. However, - // we don't know this at this point; and when the theory proof engine sees it, if it belongs - // to another theory, it won't register it with this proof. So, we need to tell the - // engine to inform us. + // If this term gets used in the final proof, we will want to register it. + // However, we don't know this at this point; and when the theory proof engine + // sees it, if it belongs to another theory, it won't register it with this + // proof. So, we need to tell the engine to inform us. - if (theory::Theory::theoryOf(term) != theory::THEORY_BV) { - Debug("pf::bv") << "\tMarking term " << term << " for future BV registration" << std::endl; + if (theory::Theory::theoryOf(term) != theory::THEORY_BV) + { + Debug("pf::bv") << "\tMarking term " << term + << " for future BV registration" << std::endl; d_proofEngine->markTermForFutureRegistration(term, theory::THEORY_BV); } } void BitVectorProof::registerAtomBB(Expr atom, Expr atom_bb) { - Debug("pf::bv") << "BitVectorProof::registerAtomBB( " << atom << ", " << atom_bb << " )" << std::endl; + Debug("pf::bv") << "BitVectorProof::registerAtomBB( " << atom + << ", " << atom_bb << " )" << std::endl; Expr def = atom.iffExpr(atom_bb); d_bbAtoms.insert(std::make_pair(atom, def)); @@ -119,9 +78,12 @@ void BitVectorProof::registerAtomBB(Expr atom, Expr atom_bb) { } void BitVectorProof::registerTerm(Expr term) { - Debug("pf::bv") << "BitVectorProof::registerTerm( " << term << " )" << std::endl; + Debug("pf::bv") << "BitVectorProof::registerTerm( " << term << " )" + << std::endl; - if (options::lfscLetification() && term.isConst()) { + if (options::lfscLetification() && term.isConst() + && term.getType().isBitVector()) + { if (d_constantLetMap.find(term) == d_constantLetMap.end()) { std::ostringstream name; name << "letBvc" << d_constantLetMap.size(); @@ -131,8 +93,8 @@ void BitVectorProof::registerTerm(Expr term) { d_usedBB.insert(term); - if (Theory::isLeafOf(term, theory::THEORY_BV) && - !term.isConst()) { + if (theory::Theory::isLeafOf(term, theory::THEORY_BV) && !term.isConst()) + { d_declarations.insert(term); } @@ -147,149 +109,32 @@ void BitVectorProof::registerTerm(Expr term) { } } -std::string BitVectorProof::getBBTermName(Expr expr) { - Debug("pf::bv") << "BitVectorProof::getBBTermName( " << expr << " ) = bt" << expr.getId() << std::endl; +std::string BitVectorProof::getBBTermName(Expr expr) +{ + Debug("pf::bv") << "BitVectorProof::getBBTermName( " << expr << " ) = bt" + << expr.getId() << std::endl; std::ostringstream os; - os << "bt"<< expr.getId(); + os << "bt" << expr.getId(); return os.str(); } -void BitVectorProof::startBVConflict(CVC4::BVMinisat::Solver::TCRef cr) { - d_resolutionProof->startResChain(cr); -} - -void BitVectorProof::startBVConflict(CVC4::BVMinisat::Solver::TLit lit) { - d_resolutionProof->startResChain(lit); -} - -void BitVectorProof::endBVConflict(const CVC4::BVMinisat::Solver::TLitVec& confl) { - Debug("pf::bv") << "BitVectorProof::endBVConflict called" << std::endl; - - std::vector<Expr> expr_confl; - for (int i = 0; i < confl.size(); ++i) { - prop::SatLiteral lit = prop::BVMinisatSatSolver::toSatLiteral(confl[i]); - Expr atom = d_cnfProof->getAtom(lit.getSatVariable()).toExpr(); - Expr expr_lit = lit.isNegated() ? atom.notExpr() : atom; - expr_confl.push_back(expr_lit); - } - - Expr conflict = utils::mkSortedExpr(kind::OR, expr_confl); - Debug("pf::bv") << "Make conflict for " << conflict << std::endl; - - if (d_bbConflictMap.find(conflict) != d_bbConflictMap.end()) { - Debug("pf::bv") << "Abort...already conflict for " << conflict << std::endl; - // This can only happen when we have eager explanations in the bv solver - // if we don't get to propagate p before ~p is already asserted - d_resolutionProof->cancelResChain(); - return; - } - - // we don't need to check for uniqueness in the sat solver then - ClauseId clause_id = d_resolutionProof->registerAssumptionConflict(confl); - d_bbConflictMap[conflict] = clause_id; - d_resolutionProof->endResChain(clause_id); - Debug("pf::bv") << "BitVectorProof::endBVConflict id" <<clause_id<< " => " << conflict << "\n"; - d_isAssumptionConflict = false; -} - -void BitVectorProof::finalizeConflicts(std::vector<Expr>& conflicts) { - - if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { - Debug("pf::bv") << "Construct full proof." << std::endl; - d_resolutionProof->constructProof(); - return; - } - - for (unsigned i = 0; i < conflicts.size(); ++i) { - Expr confl = conflicts[i]; - Debug("pf::bv") << "Finalize conflict #" << i << ": " << confl << std::endl; - - // Special case: if the conflict has a (true) or a (not false) in it, it is trivial... - bool ignoreConflict = false; - if ((confl.isConst() && confl.getConst<bool>()) || - (confl.getKind() == kind::NOT && confl[0].isConst() && !confl[0].getConst<bool>())) { - ignoreConflict = true; - } else if (confl.getKind() == kind::OR) { - for (unsigned k = 0; k < confl.getNumChildren(); ++k) { - if ((confl[k].isConst() && confl[k].getConst<bool>()) || - (confl[k].getKind() == kind::NOT && confl[k][0].isConst() && !confl[k][0].getConst<bool>())) { - ignoreConflict = true; - } - } - } - if (ignoreConflict) { - Debug("pf::bv") << "Ignoring conflict due to (true) or (not false)" << std::endl; - continue; - } - - if (d_bbConflictMap.find(confl) != d_bbConflictMap.end()) { - ClauseId id = d_bbConflictMap[confl]; - d_resolutionProof->collectClauses(id); - } else { - // There is no exact match for our conflict, but maybe it is a subset of another conflict - ExprToClauseId::const_iterator it; - bool matchFound = false; - for (it = d_bbConflictMap.begin(); it != d_bbConflictMap.end(); ++it) { - Expr possibleMatch = it->first; - if (possibleMatch.getKind() != kind::OR) { - // This is a single-node conflict. If this node is in the conflict we're trying to prove, - // we have a match. - for (unsigned k = 0; k < confl.getNumChildren(); ++k) { - if (confl[k] == possibleMatch) { - matchFound = true; - d_resolutionProof->collectClauses(it->second); - break; - } - } - } else { - if (possibleMatch.getNumChildren() > confl.getNumChildren()) - continue; - - unsigned k = 0; - bool matching = true; - for (unsigned j = 0; j < possibleMatch.getNumChildren(); ++j) { - // j is the index in possibleMatch - // k is the index in confl - while (k < confl.getNumChildren() && confl[k] != possibleMatch[j]) { - ++k; - } - if (k == confl.getNumChildren()) { - // We couldn't find a match for possibleMatch[j], so not a match - matching = false; - break; - } - } - - if (matching) { - Debug("pf::bv") << "Collecting info from a sub-conflict" << std::endl; - d_resolutionProof->collectClauses(it->second); - matchFound = true; - break; - } - } - } - - if (!matchFound) { - Debug("pf::bv") << "Do not collect clauses for " << confl << std::endl - << "Dumping existing conflicts:" << std::endl; - - i = 0; - for (it = d_bbConflictMap.begin(); it != d_bbConflictMap.end(); ++it) { - ++i; - Debug("pf::bv") << "\tConflict #" << i << ": " << it->first << std::endl; - } - - Unreachable(); - } - } - } +void BitVectorProof::initCnfProof(prop::CnfStream* cnfStream, + context::Context* cnf) +{ + Assert(d_cnfProof == nullptr); + d_cnfProof.reset(new LFSCCnfProof(cnfStream, cnf, "bb")); } -void LFSCBitVectorProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) { - Debug("pf::bv") << std::endl << "(pf::bv) LFSCBitVectorProof::printOwnedTerm( " << term << " ), theory is: " - << Theory::theoryOf(term) << std::endl; +void BitVectorProof::printOwnedTerm(Expr term, + std::ostream& os, + const ProofLetMap& map) +{ + Debug("pf::bv") << std::endl + << "(pf::bv) BitVectorProof::printOwnedTerm( " << term + << " ), theory is: " << theory::Theory::theoryOf(term) + << std::endl; - Assert (Theory::theoryOf(term) == THEORY_BV); + Assert(theory::Theory::theoryOf(term) == theory::THEORY_BV); // peel off eager bit-blasting trick if (term.getKind() == kind::BITVECTOR_EAGER_ATOM) { @@ -380,21 +225,24 @@ void LFSCBitVectorProof::printOwnedTerm(Expr term, std::ostream& os, const Proof } } -void LFSCBitVectorProof::printBitOf(Expr term, std::ostream& os, const ProofLetMap& map) { +void BitVectorProof::printBitOf(Expr term, + std::ostream& os, + const ProofLetMap& map) +{ Assert (term.getKind() == kind::BITVECTOR_BITOF); unsigned bit = term.getOperator().getConst<BitVectorBitOf>().bitIndex; Expr var = term[0]; - Debug("pf::bv") << "LFSCBitVectorProof::printBitOf( " << term << " ), " - << "bit = " << bit - << ", var = " << var << std::endl; + Debug("pf::bv") << "BitVectorProof::printBitOf( " << term << " ), " + << "bit = " << bit << ", var = " << var << std::endl; os << "(bitof "; os << d_exprToVariableName[var]; os << " " << bit << ")"; } -void LFSCBitVectorProof::printConstant(Expr term, std::ostream& os) { +void BitVectorProof::printConstant(Expr term, std::ostream& os) +{ Assert (term.isConst()); os << "(a_bv " << utils::getSize(term) << " "; @@ -413,7 +261,10 @@ void LFSCBitVectorProof::printConstant(Expr term, std::ostream& os) { } } -void LFSCBitVectorProof::printOperatorNary(Expr term, std::ostream& os, const ProofLetMap& map) { +void BitVectorProof::printOperatorNary(Expr term, + std::ostream& os, + const ProofLetMap& map) +{ std::string op = utils::toLFSCKindTerm(term); std::ostringstream paren; std::string holes = term.getKind() == kind::BITVECTOR_CONCAT ? "_ _ " : ""; @@ -431,7 +282,10 @@ void LFSCBitVectorProof::printOperatorNary(Expr term, std::ostream& os, const Pr } } -void LFSCBitVectorProof::printOperatorUnary(Expr term, std::ostream& os, const ProofLetMap& map) { +void BitVectorProof::printOperatorUnary(Expr term, + std::ostream& os, + const ProofLetMap& map) +{ os <<"("; os << utils::toLFSCKindTerm(term) << " " << utils::getSize(term) <<" "; os << " "; @@ -439,7 +293,10 @@ void LFSCBitVectorProof::printOperatorUnary(Expr term, std::ostream& os, const P os <<")"; } -void LFSCBitVectorProof::printPredicate(Expr term, std::ostream& os, const ProofLetMap& map) { +void BitVectorProof::printPredicate(Expr term, + std::ostream& os, + const ProofLetMap& map) +{ os <<"("; os << utils::toLFSCKindTerm(term) << " " << utils::getSize(term[0]) <<" "; os << " "; @@ -449,7 +306,10 @@ void LFSCBitVectorProof::printPredicate(Expr term, std::ostream& os, const Proof os <<")"; } -void LFSCBitVectorProof::printOperatorParametric(Expr term, std::ostream& os, const ProofLetMap& map) { +void BitVectorProof::printOperatorParametric(Expr term, + std::ostream& os, + const ProofLetMap& map) +{ os <<"("; os << utils::toLFSCKindTerm(term) << " " << utils::getSize(term) <<" "; os <<" "; @@ -477,185 +337,25 @@ void LFSCBitVectorProof::printOperatorParametric(Expr term, std::ostream& os, co os <<")"; } -void LFSCBitVectorProof::printOwnedSort(Type type, std::ostream& os) { - Debug("pf::bv") << std::endl << "(pf::bv) LFSCBitVectorProof::printOwnedSort( " << type << " )" << std::endl; +void BitVectorProof::printOwnedSort(Type type, std::ostream& os) +{ + Debug("pf::bv") << std::endl + << "(pf::bv) BitVectorProof::printOwnedSort( " << type << " )" + << std::endl; Assert (type.isBitVector()); unsigned width = utils::getSize(type); os << "(BitVec " << width << ")"; } -void LFSCBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map) { - Debug("pf::bv") << "(pf::bv) LFSCBitVectorProof::printTheoryLemmaProof called" << std::endl; - Expr conflict = utils::mkSortedExpr(kind::OR, lemma); - Debug("pf::bv") << "\tconflict = " << conflict << std::endl; - - if (d_bbConflictMap.find(conflict) != d_bbConflictMap.end()) { - std::ostringstream lemma_paren; - for (unsigned i = 0; i < lemma.size(); ++i) { - Expr lit = lemma[i]; - - if (lit.getKind() == kind::NOT) { - os << "(intro_assump_t _ _ _ "; - } else { - os << "(intro_assump_f _ _ _ "; - } - lemma_paren <<")"; - // print corresponding literal in main sat solver - ProofManager* pm = ProofManager::currentPM(); - CnfProof* cnf = pm->getCnfProof(); - prop::SatLiteral main_lit = cnf->getLiteral(lit); - os << pm->getLitName(main_lit); - os <<" "; - // print corresponding literal in bv sat solver - prop::SatVariable bb_var = d_cnfProof->getLiteral(lit).getSatVariable(); - os << pm->getAtomName(bb_var, "bb"); - os <<"(\\ unit"<<bb_var<<"\n"; - lemma_paren <<")"; - } - Expr lem = utils::mkOr(lemma); - Assert (d_bbConflictMap.find(lem) != d_bbConflictMap.end()); - ClauseId lemma_id = d_bbConflictMap[lem]; - proof::LFSCProofPrinter::printAssumptionsResolution( - d_resolutionProof, lemma_id, os, lemma_paren); - os <<lemma_paren.str(); - } else { - - Debug("pf::bv") << "Found a non-recorded conflict. Looking for a matching sub-conflict..." - << std::endl; - - bool matching; - - ExprToClauseId::const_iterator it; - unsigned i = 0; - for (it = d_bbConflictMap.begin(); it != d_bbConflictMap.end(); ++it) { - // Our conflict is sorted, and the records are also sorted. - ++i; - Expr possibleMatch = it->first; - - if (possibleMatch.getKind() != kind::OR) { - // This is a single-node conflict. If this node is in the conflict we're trying to prove, - // we have a match. - matching = false; - - for (unsigned k = 0; k < conflict.getNumChildren(); ++k) { - if (conflict[k] == possibleMatch) { - matching = true; - break; - } - } - } else { - if (possibleMatch.getNumChildren() > conflict.getNumChildren()) - continue; - - unsigned k = 0; - - matching = true; - for (unsigned j = 0; j < possibleMatch.getNumChildren(); ++j) { - // j is the index in possibleMatch - // k is the index in conflict - while (k < conflict.getNumChildren() && conflict[k] != possibleMatch[j]) { - ++k; - } - if (k == conflict.getNumChildren()) { - // We couldn't find a match for possibleMatch[j], so not a match - matching = false; - break; - } - } - } - - if (matching) { - Debug("pf::bv") << "Found a match with conflict #" << i << ": " << std::endl << possibleMatch << std::endl; - // The rest is just a copy of the usual handling, if a precise match is found. - // We only use the literals that appear in the matching conflict, though, and not in the - // original lemma - as these may not have even been bit blasted! - std::ostringstream lemma_paren; - - if (possibleMatch.getKind() == kind::OR) { - for (unsigned i = 0; i < possibleMatch.getNumChildren(); ++i) { - Expr lit = possibleMatch[i]; - - if (lit.getKind() == kind::NOT) { - os << "(intro_assump_t _ _ _ "; - } else { - os << "(intro_assump_f _ _ _ "; - } - lemma_paren <<")"; - // print corresponding literal in main sat solver - ProofManager* pm = ProofManager::currentPM(); - CnfProof* cnf = pm->getCnfProof(); - prop::SatLiteral main_lit = cnf->getLiteral(lit); - os << pm->getLitName(main_lit); - os <<" "; - // print corresponding literal in bv sat solver - prop::SatVariable bb_var = d_cnfProof->getLiteral(lit).getSatVariable(); - os << pm->getAtomName(bb_var, "bb"); - os <<"(\\ unit"<<bb_var<<"\n"; - lemma_paren <<")"; - } - } else { - // The conflict only consists of one node, either positive or negative. - Expr lit = possibleMatch; - if (lit.getKind() == kind::NOT) { - os << "(intro_assump_t _ _ _ "; - } else { - os << "(intro_assump_f _ _ _ "; - } - lemma_paren <<")"; - // print corresponding literal in main sat solver - ProofManager* pm = ProofManager::currentPM(); - CnfProof* cnf = pm->getCnfProof(); - prop::SatLiteral main_lit = cnf->getLiteral(lit); - os << pm->getLitName(main_lit); - os <<" "; - // print corresponding literal in bv sat solver - prop::SatVariable bb_var = d_cnfProof->getLiteral(lit).getSatVariable(); - os << pm->getAtomName(bb_var, "bb"); - os <<"(\\ unit"<<bb_var<<"\n"; - lemma_paren <<")"; - } - - ClauseId lemma_id = it->second; - proof::LFSCProofPrinter::printAssumptionsResolution( - d_resolutionProof, lemma_id, os, lemma_paren); - os <<lemma_paren.str(); - - return; - } - } - - // We failed to find a matching sub conflict. The last hope is that the - // conflict has a FALSE assertion in it; this can happen in some corner cases, - // where the FALSE is the result of a rewrite. - - for (unsigned i = 0; i < lemma.size(); ++i) { - if (lemma[i].getKind() == kind::NOT && lemma[i][0] == utils::mkFalse()) { - Debug("pf::bv") << "Lemma has a (not false) literal" << std::endl; - os << "(clausify_false "; - os << ProofManager::getLitName(lemma[i]); - os << ")"; - return; - } - } - - Debug("pf::bv") << "Failed to find a matching sub-conflict..." << std::endl - << "Dumping existing conflicts:" << std::endl; - - i = 0; - for (it = d_bbConflictMap.begin(); it != d_bbConflictMap.end(); ++it) { - ++i; - Debug("pf::bv") << "\tConflict #" << i << ": " << it->first << std::endl; - } - - Unreachable(); - } -} - -void LFSCBitVectorProof::printSortDeclarations(std::ostream& os, std::ostream& paren) { +void BitVectorProof::printSortDeclarations(std::ostream& os, + std::ostream& paren) +{ // Nothing to do here at this point. } -void LFSCBitVectorProof::printTermDeclarations(std::ostream& os, std::ostream& paren) { +void BitVectorProof::printTermDeclarations(std::ostream& os, + std::ostream& paren) +{ ExprSet::const_iterator it = d_declarations.begin(); ExprSet::const_iterator end = d_declarations.end(); for (; it != end; ++it) { @@ -671,7 +371,9 @@ void LFSCBitVectorProof::printTermDeclarations(std::ostream& os, std::ostream& p } } -void LFSCBitVectorProof::printDeferredDeclarations(std::ostream& os, std::ostream& paren) { +void BitVectorProof::printDeferredDeclarations(std::ostream& os, + std::ostream& paren) +{ if (options::lfscLetification()) { os << std::endl << ";; BV const letification\n" << std::endl; std::map<Expr,std::string>::const_iterator it; @@ -694,7 +396,10 @@ void LFSCBitVectorProof::printDeferredDeclarations(std::ostream& os, std::ostrea } } -void LFSCBitVectorProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap) { +void BitVectorProof::printAliasingDeclarations(std::ostream& os, + std::ostream& paren, + const ProofLetMap& globalLetMap) +{ // Print "trust" statements to bind complex bv variables to their associated terms ExprToString::const_iterator it = d_assignedAliases.begin(); @@ -720,13 +425,15 @@ void LFSCBitVectorProof::printAliasingDeclarations(std::ostream& os, std::ostrea os << "\n"; } -void LFSCBitVectorProof::printTermBitblasting(Expr term, std::ostream& os) { +void BitVectorProof::printTermBitblasting(Expr term, std::ostream& os) +{ // TODO: once we have the operator elimination rules remove those that we // eliminated Assert (term.getType().isBitVector()); Kind kind = term.getKind(); - if (Theory::isLeafOf(term, theory::THEORY_BV) && !term.isConst()) { + if (theory::Theory::isLeafOf(term, theory::THEORY_BV) && !term.isConst()) + { // A term is a leaf if it has no children, or if it belongs to another theory os << "(bv_bbl_var " << utils::getSize(term) << " " << d_exprToVariableName[term]; os << " _)"; @@ -857,12 +564,14 @@ void LFSCBitVectorProof::printTermBitblasting(Expr term, std::ostream& os) { return; } - default: - Unreachable("LFSCBitVectorProof Unknown operator"); + default: Unreachable("BitVectorProof Unknown operator"); } } -void LFSCBitVectorProof::printAtomBitblasting(Expr atom, std::ostream& os, bool swap) { +void BitVectorProof::printAtomBitblasting(Expr atom, + std::ostream& os, + bool swap) +{ Kind kind = atom.getKind(); switch(kind) { case kind::BITVECTOR_ULT : @@ -888,12 +597,12 @@ void LFSCBitVectorProof::printAtomBitblasting(Expr atom, std::ostream& os, bool return; } - default: - Unreachable("LFSCBitVectorProof Unknown atom kind"); + default: Unreachable("BitVectorProof Unknown atom kind"); } } -void LFSCBitVectorProof::printAtomBitblastingToFalse(Expr atom, std::ostream& os) { +void BitVectorProof::printAtomBitblastingToFalse(Expr atom, std::ostream& os) +{ Assert(atom.getKind() == kind::EQUAL); os << "(bv_bbl_=_false"; @@ -907,15 +616,16 @@ void LFSCBitVectorProof::printAtomBitblastingToFalse(Expr atom, std::ostream& os os << ")"; } -void LFSCBitVectorProof::printBitblasting(std::ostream& os, std::ostream& paren) { +void BitVectorProof::printBitblasting(std::ostream& os, std::ostream& paren) +{ // bit-blast terms { - Debug("pf::bv") << "LFSCBitVectorProof::printBitblasting: the bitblasted terms are: " << std::endl; + Debug("pf::bv") + << "BitVectorProof::printBitblasting: the bitblasted terms are: " + << std::endl; std::vector<Expr>::const_iterator it = d_bbTerms.begin(); std::vector<Expr>::const_iterator end = d_bbTerms.end(); - Assert(options::bitblastMode() != theory::bv::BITBLAST_MODE_EAGER); - for (; it != end; ++it) { if (d_usedBB.find(*it) == d_usedBB.end()) { Debug("pf::bv") << "\t" << *it << "\t(UNUSED)" << std::endl; @@ -999,52 +709,13 @@ void LFSCBitVectorProof::printBitblasting(std::ostream& os, std::ostream& paren) } } -void LFSCBitVectorProof::calculateAtomsInBitblastingProof() { - // Collect the input clauses used - IdToSatClause used_lemmas; - IdToSatClause used_inputs; - d_resolutionProof->collectClausesUsed(used_inputs, used_lemmas); - d_cnfProof->collectAtomsForClauses(used_inputs, d_atomsInBitblastingProof); - Assert(used_lemmas.empty()); -} - -const std::set<Node>* LFSCBitVectorProof::getAtomsInBitblastingProof() { +const std::set<Node>* BitVectorProof::getAtomsInBitblastingProof() +{ return &d_atomsInBitblastingProof; } -void LFSCBitVectorProof::printResolutionProof(std::ostream& os, - std::ostream& paren, - ProofLetMap& letMap) { - // print mapping between theory atoms and internal SAT variables - os << std::endl << ";; BB atom mapping\n" << std::endl; - - std::set<Node>::iterator atomIt; - Debug("pf::bv") << std::endl << "BV Dumping atoms from inputs: " << std::endl << std::endl; - for (atomIt = d_atomsInBitblastingProof.begin(); atomIt != d_atomsInBitblastingProof.end(); ++atomIt) { - Debug("pf::bv") << "\tAtom: " << *atomIt << std::endl; - } - Debug("pf::bv") << std::endl; - - // first print bit-blasting - printBitblasting(os, paren); - - // print CNF conversion proof for bit-blasted facts - IdToSatClause used_lemmas; - IdToSatClause used_inputs; - d_resolutionProof->collectClausesUsed(used_inputs, used_lemmas); - - d_cnfProof->printAtomMapping(d_atomsInBitblastingProof, os, paren, letMap); - os << std::endl << ";; Bit-blasting definitional clauses \n" << std::endl; - for (IdToSatClause::iterator it = used_inputs.begin(); - it != used_inputs.end(); ++it) { - d_cnfProof->printCnfProofForClause(it->first, it->second, os, paren); - } - - os << std::endl << " ;; Bit-blasting learned clauses \n" << std::endl; - proof::LFSCProofPrinter::printResolutions(d_resolutionProof, os, paren); -} - -std::string LFSCBitVectorProof::assignAlias(Expr expr) { +std::string BitVectorProof::assignAlias(Expr expr) +{ Assert(d_exprToVariableName.find(expr) == d_exprToVariableName.end()); std::stringstream ss; @@ -1054,11 +725,14 @@ std::string LFSCBitVectorProof::assignAlias(Expr expr) { return ss.str(); } -bool LFSCBitVectorProof::hasAlias(Expr expr) { +bool BitVectorProof::hasAlias(Expr expr) +{ return d_assignedAliases.find(expr) != d_assignedAliases.end(); } -void LFSCBitVectorProof::printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap) { +void BitVectorProof::printConstantDisequalityProof( + std::ostream& os, Expr c1, Expr c2, const ProofLetMap& globalLetMap) +{ Assert (c1.isConst()); Assert (c2.isConst()); Assert (utils::getSize(c1) == utils::getSize(c2)); @@ -1088,7 +762,10 @@ void LFSCBitVectorProof::printConstantDisequalityProof(std::ostream& os, Expr c1 os << ")"; } -void LFSCBitVectorProof::printRewriteProof(std::ostream& os, const Node &n1, const Node &n2) { +void BitVectorProof::printRewriteProof(std::ostream& os, + const Node& n1, + const Node& n2) +{ ProofLetMap emptyMap; os << "(rr_bv_default "; d_proofEngine->printBoundTerm(n2.toExpr(), os, emptyMap); @@ -1097,4 +774,4 @@ void LFSCBitVectorProof::printRewriteProof(std::ostream& os, const Node &n1, con os << ")"; } -} /* namespace CVC4 */ +} // namespace CVC4 diff --git a/src/proof/bitvector_proof.h b/src/proof/bitvector_proof.h index 63f1cdf63..466efa6a7 100644 --- a/src/proof/bitvector_proof.h +++ b/src/proof/bitvector_proof.h @@ -9,118 +9,166 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Bitvector proof + ** \brief Bitvector proof base class ** - ** Bitvector proof + ** Contains code (e.g. proof printing code) which is common to all bitvector + *proofs. **/ #include "cvc4_private.h" -#ifndef __CVC4__BITVECTOR__PROOF_H -#define __CVC4__BITVECTOR__PROOF_H +#ifndef __CVC4__BITVECTOR_PROOF_H +#define __CVC4__BITVECTOR_PROOF_H -#include <iostream> #include <set> -#include <sstream> #include <unordered_map> #include <unordered_set> #include <vector> - #include "expr/expr.h" +#include "proof/cnf_proof.h" #include "proof/theory_proof.h" -#include "prop/bvminisat/core/Solver.h" - +#include "theory/bv/bitblast/bitblaster.h" +#include "theory/bv/theory_bv.h" namespace CVC4 { -namespace prop { -class CnfStream; -} /* namespace CVC4::prop */ - -namespace theory { -namespace bv { -class TheoryBV; -template <class T> class TBitblaster; -} /* namespace CVC4::theory::bv */ -} /* namespace CVC4::theory */ - -class CnfProof; -} /* namespace CVC4 */ - -namespace CVC4 { - -template <class Solver> class TSatProof; -typedef TSatProof< CVC4::BVMinisat::Solver> BVSatProof; - typedef std::unordered_set<Expr, ExprHashFunction> ExprSet; typedef std::unordered_map<Expr, ClauseId, ExprHashFunction> ExprToClauseId; typedef std::unordered_map<Expr, unsigned, ExprHashFunction> ExprToId; typedef std::unordered_map<Expr, Expr, ExprHashFunction> ExprToExpr; typedef std::unordered_map<Expr, std::string, ExprHashFunction> ExprToString; -class BitVectorProof : public TheoryProof { -protected: +/** + * A bitvector proof is best understood as having + * + * 1. A declaration of a "bitblasted formulas" -- boolean formulas + * that are each translations of a BV-literal (a comparison between BVs). + * + * (and a proof that each "bitblasted formula" is implied by the + * corresponding BV literal) + * + * 2. A declaration of a cnf formula equisatisfiable to the bitblasted + * formula + * + * (and a proof that each clause is implied by some bitblasted formula) + * + * 3. A proof of UNSAT from the clauses. + * + * This class is responsible for 1 & 2. The proof of UNSAT is delegated to a + * subclass. + */ +class BitVectorProof : public TheoryProof +{ + protected: + BitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine); + virtual ~BitVectorProof(){}; + + // Set of BV variables in the input. (e.g. "a" in [ a = 000 ] ^ [ a == 001 ]) ExprSet d_declarations; - ExprSet d_usedBB; // terms and formulas that are actually relevant to the proof + // terms and formulas that are actually relevant to the proof + ExprSet d_usedBB; + + ExprSet d_seenBBTerms; // terms that need to be bit-blasted + std::vector<Expr> d_bbTerms; // order of bit-blasting - ExprSet d_seenBBTerms; // terms that need to be bit-blasted - std::vector<Expr> d_bbTerms; // order of bit-blasting - ExprToExpr d_bbAtoms; // atoms that need to be bit-blasted + /** atoms that need to be bit-blasted, + * BV-literals -> (BV-literals <=> bool formula) + * where a BV literal is a signed or unsigned comparison. + */ + ExprToExpr d_bbAtoms; // map from Expr representing normalized lemma to ClauseId in SAT solver ExprToClauseId d_bbConflictMap; - BVSatProof* d_resolutionProof; - CnfProof* d_cnfProof; - - bool d_isAssumptionConflict; theory::bv::TBitblaster<Node>* d_bitblaster; + + /** In an LFSC proof the manifestation of this expression bit-level + * representation will have a string name. This method returns that name. + */ std::string getBBTermName(Expr expr); - std::map<Expr,std::string> d_constantLetMap; + /** A mapping from constant BV terms to identifiers that will refer to them in + * an LFSC proof, if constant-letification is enabled. + */ + std::map<Expr, std::string> d_constantLetMap; + + /** Should we introduced identifiers to refer to BV constant terms? It may + * reduce the textual size of a proof! + */ bool d_useConstantLetification; - theory::TheoryId getTheoryId() override; - context::Context d_fakeContext; -public: - BitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine); - void initSatProof(CVC4::BVMinisat::Solver* solver); - void initCnfProof(prop::CnfStream* cnfStream, context::Context* ctx); - void setBitblaster(theory::bv::TBitblaster<Node>* bb); + /** Temporary storage for the set of nodes in the bitblasted formula which + * correspond to CNF variables eventually used in the proof of unsat on the + * CNF formula + */ + std::set<Node> d_atomsInBitblastingProof; - BVSatProof* getSatProof(); - CnfProof* getCnfProof() {return d_cnfProof; } - void finalizeConflicts(std::vector<Expr>& conflicts); + /** + * Prints out + * (a) a declaration of bit-level interpretations corresponding to bits in + * the input BV terms. + * (b) a proof that the each BV literal entails a boolean formula on + * bitof expressions. + */ + void printBitblasting(std::ostream& os, std::ostream& paren); - void startBVConflict(CVC4::BVMinisat::Solver::TCRef cr); - void startBVConflict(CVC4::BVMinisat::Solver::TLit lit); /** - * All the - * - * @param confl an inconsistent set of bv literals + * The proof that the bit-blasted SAT formula is correctly converted to CNF */ - void endBVConflict(const BVMinisat::Solver::TLitVec& confl); - void markAssumptionConflict() { d_isAssumptionConflict = true; } - bool isAssumptionConflict() { return d_isAssumptionConflict; } + std::unique_ptr<CnfProof> d_cnfProof; + + public: + void printOwnedTerm(Expr term, + std::ostream& os, + const ProofLetMap& map) override; + + void printOwnedSort(Type type, std::ostream& os) override; + + /** + * Populate the d_atomsInBitblastingProof member. + * See its documentation + */ + virtual void calculateAtomsInBitblastingProof() = 0; + + /** + * Read the d_atomsInBitblastingProof member. + * See its documentation. + */ + const std::set<Node>* getAtomsInBitblastingProof(); void registerTermBB(Expr term); + + /** + * Informs the proof that the `atom` predicate was bitblasted into the + * `atom_bb` term. + * + * The `atom` term must be a comparison of bitvectors, and the `atom_bb` term + * a boolean formula on bitof expressions + */ void registerAtomBB(Expr atom, Expr atom_bb); void registerTerm(Expr term) override; - virtual void printTermBitblasting(Expr term, std::ostream& os) = 0; - virtual void printAtomBitblasting(Expr term, std::ostream& os, bool swap) = 0; - virtual void printAtomBitblastingToFalse(Expr term, std::ostream& os) = 0; + /** + * This must be done before registering any terms or atoms, since the CNF + * proof must reflect the result of bitblasting those + */ + virtual void initCnfProof(prop::CnfStream* cnfStream, context::Context* ctx); - virtual void printBitblasting(std::ostream& os, std::ostream& paren) = 0; - virtual void printResolutionProof(std::ostream& os, std::ostream& paren, ProofLetMap& letMap) = 0; - virtual const std::set<Node>* getAtomsInBitblastingProof() = 0; - virtual void calculateAtomsInBitblastingProof() = 0; -}; + CnfProof* getCnfProof() { return d_cnfProof.get(); } + + void setBitblaster(theory::bv::TBitblaster<Node>* bb); -class LFSCBitVectorProof: public BitVectorProof { + private: + ExprToString d_exprToVariableName; + + ExprToString d_assignedAliases; + std::map<std::string, std::string> d_aliasToBindDeclaration; + std::string assignAlias(Expr expr); + bool hasAlias(Expr expr); + // Functions for printing various BV terms. Helpers for BV's `printOwnedTerm` void printConstant(Expr term, std::ostream& os); void printOperatorNary(Expr term, std::ostream& os, const ProofLetMap& map); void printOperatorUnary(Expr term, std::ostream& os, const ProofLetMap& map); @@ -128,29 +176,19 @@ class LFSCBitVectorProof: public BitVectorProof { void printOperatorParametric(Expr term, std::ostream& os, const ProofLetMap& map); void printBitOf(Expr term, std::ostream& os, const ProofLetMap& map); - ExprToString d_exprToVariableName; - ExprToString d_assignedAliases; - std::map<std::string, std::string> d_aliasToBindDeclaration; - std::string assignAlias(Expr expr); - bool hasAlias(Expr expr); + /** + * Prints the LFSC construction of a bblast_term for `term` + */ + void printTermBitblasting(Expr term, std::ostream& os); - std::set<Node> d_atomsInBitblastingProof; + /** + * For a given BV-atom (a comparison), prints a proof that that comparison + * holds iff the bitblasted equivalent of it holds. + * Uses a side-condidition to do the bit-blasting. + */ + void printAtomBitblasting(Expr term, std::ostream& os, bool swap); + void printAtomBitblastingToFalse(Expr term, std::ostream& os); -public: - LFSCBitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine) - :BitVectorProof(bv, proofEngine) - {} - void printOwnedTerm(Expr term, - std::ostream& os, - const ProofLetMap& map) override; - void printOwnedSort(Type type, std::ostream& os) override; - void printTermBitblasting(Expr term, std::ostream& os) override; - void printAtomBitblasting(Expr term, std::ostream& os, bool swap) override; - void printAtomBitblastingToFalse(Expr term, std::ostream& os) override; - void printTheoryLemmaProof(std::vector<Expr>& lemma, - std::ostream& os, - std::ostream& paren, - const ProofLetMap& map) override; void printSortDeclarations(std::ostream& os, std::ostream& paren) override; void printTermDeclarations(std::ostream& os, std::ostream& paren) override; void printDeferredDeclarations(std::ostream& os, @@ -158,12 +196,7 @@ public: void printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap& globalLetMap) override; - void printBitblasting(std::ostream& os, std::ostream& paren) override; - void printResolutionProof(std::ostream& os, - std::ostream& paren, - ProofLetMap& letMap) override; - void calculateAtomsInBitblastingProof() override; - const std::set<Node>* getAtomsInBitblastingProof() override; + void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index e7b00068a..9878972bf 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -21,11 +21,11 @@ #include "context/context.h" #include "options/bv_options.h" #include "options/proof_options.h" -#include "proof/bitvector_proof.h" #include "proof/clause_id.h" #include "proof/cnf_proof.h" #include "proof/lfsc_proof_printer.h" #include "proof/proof_utils.h" +#include "proof/resolution_bitvector_proof.h" #include "proof/sat_proof_implementation.h" #include "proof/theory_proof.h" #include "smt/smt_engine.h" @@ -116,10 +116,11 @@ UFProof* ProofManager::getUfProof() { return (UFProof*)pf; } -BitVectorProof* ProofManager::getBitVectorProof() { +proof::ResolutionBitVectorProof* ProofManager::getBitVectorProof() +{ Assert (options::proof()); TheoryProof* pf = getTheoryProofEngine()->getTheoryProof(theory::THEORY_BV); - return (BitVectorProof*)pf; + return static_cast<proof::ResolutionBitVectorProof*>(pf); } ArrayProof* ProofManager::getArrayProof() { @@ -558,8 +559,6 @@ void LFSCProof::toStream(std::ostream& out, const ProofLetMap& map) const void LFSCProof::toStream(std::ostream& out) const { - Assert(options::bitblastMode() != theory::bv::BITBLAST_MODE_EAGER); - Assert(!d_satProof->proofConstructed()); d_satProof->constructProof(); @@ -729,6 +728,7 @@ void LFSCProof::toStream(std::ostream& out) const d_theoryProof->printTheoryLemmas(used_lemmas, out, paren, globalLetMap); Debug("pf::pm") << "Proof manager: printing theory lemmas DONE!" << std::endl; + out << ";; Printing final unsat proof \n"; if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER && ProofManager::getBitVectorProof()) { proof::LFSCProofPrinter::printResolutionEmptyClause( ProofManager::getBitVectorProof()->getSatProof(), out, paren); diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h index 0342288fe..82efbab0f 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -69,7 +69,10 @@ class TheoryProof; class UFProof; class ArithProof; class ArrayProof; -class BitVectorProof; + +namespace proof { +class ResolutionBitVectorProof; +} template <class Solver> class LFSCSatProof; typedef TSatProof<CVC4::Minisat::Solver> CoreSatProof; @@ -77,7 +80,6 @@ typedef TSatProof<CVC4::Minisat::Solver> CoreSatProof; class LFSCCnfProof; class LFSCTheoryProofEngine; class LFSCUFProof; -class LFSCBitVectorProof; class LFSCRewriterProof; namespace prop { @@ -189,7 +191,7 @@ public: static TheoryProofEngine* getTheoryProofEngine(); static TheoryProof* getTheoryProof( theory::TheoryId id ); static UFProof* getUfProof(); - static BitVectorProof* getBitVectorProof(); + static proof::ResolutionBitVectorProof* getBitVectorProof(); static ArrayProof* getArrayProof(); static ArithProof* getArithProof(); diff --git a/src/proof/resolution_bitvector_proof.cpp b/src/proof/resolution_bitvector_proof.cpp new file mode 100644 index 000000000..667d630f8 --- /dev/null +++ b/src/proof/resolution_bitvector_proof.cpp @@ -0,0 +1,522 @@ +/********************* */ +/*! \file resolution_bitvector_proof.cpp + ** \verbatim + ** Top contributors (to current version): + ** Liana Hadarean, Guy Katz, Paul Meng + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** [[ Add lengthier description here ]] + + ** \todo document this file + +**/ + +#include "proof/resolution_bitvector_proof.h" +#include "options/bv_options.h" +#include "options/proof_options.h" +#include "proof/array_proof.h" +#include "proof/bitvector_proof.h" +#include "proof/clause_id.h" +#include "proof/lfsc_proof_printer.h" +#include "proof/proof_output_channel.h" +#include "proof/proof_utils.h" +#include "proof/sat_proof_implementation.h" +#include "prop/bvminisat/bvminisat.h" +#include "theory/bv/bitblast/bitblaster.h" +#include "theory/bv/theory_bv.h" +#include "theory/bv/theory_bv_rewrite_rules.h" + +#include <iostream> +#include <sstream> + +using namespace CVC4::theory; +using namespace CVC4::theory::bv; + +namespace CVC4 { + +namespace proof { + +ResolutionBitVectorProof::ResolutionBitVectorProof( + theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine) + : BitVectorProof(bv, proofEngine), + d_resolutionProof(), + d_isAssumptionConflict(false) +{ +} + +void ResolutionBitVectorProof::initSatProof(CVC4::BVMinisat::Solver* solver) +{ + Assert(d_resolutionProof == NULL); + d_resolutionProof.reset(new BVSatProof(solver, &d_fakeContext, "bb", true)); +} + +theory::TheoryId ResolutionBitVectorProof::getTheoryId() +{ + return theory::THEORY_BV; +} + +void ResolutionBitVectorProof::initCnfProof(prop::CnfStream* cnfStream, + context::Context* cnf) +{ + Assert(d_resolutionProof != NULL); + BitVectorProof::initCnfProof(cnfStream, cnf); + + // true and false have to be setup in a special way + Node true_node = NodeManager::currentNM()->mkConst<bool>(true); + Node false_node = NodeManager::currentNM()->mkConst<bool>(false).notNode(); + + d_cnfProof->pushCurrentAssertion(true_node); + d_cnfProof->pushCurrentDefinition(true_node); + d_cnfProof->registerConvertedClause(d_resolutionProof->getTrueUnit()); + d_cnfProof->popCurrentAssertion(); + d_cnfProof->popCurrentDefinition(); + + d_cnfProof->pushCurrentAssertion(false_node); + d_cnfProof->pushCurrentDefinition(false_node); + d_cnfProof->registerConvertedClause(d_resolutionProof->getFalseUnit()); + d_cnfProof->popCurrentAssertion(); + d_cnfProof->popCurrentDefinition(); +} + +BVSatProof* ResolutionBitVectorProof::getSatProof() +{ + Assert(d_resolutionProof != NULL); + return d_resolutionProof.get(); +} + +void ResolutionBitVectorProof::startBVConflict( + CVC4::BVMinisat::Solver::TCRef cr) +{ + d_resolutionProof->startResChain(cr); +} + +void ResolutionBitVectorProof::startBVConflict( + CVC4::BVMinisat::Solver::TLit lit) +{ + d_resolutionProof->startResChain(lit); +} + +void ResolutionBitVectorProof::endBVConflict( + const CVC4::BVMinisat::Solver::TLitVec& confl) +{ + Debug("pf::bv") << "ResolutionBitVectorProof::endBVConflict called" + << std::endl; + + std::vector<Expr> expr_confl; + for (int i = 0; i < confl.size(); ++i) + { + prop::SatLiteral lit = prop::BVMinisatSatSolver::toSatLiteral(confl[i]); + Expr atom = d_cnfProof->getAtom(lit.getSatVariable()).toExpr(); + Expr expr_lit = lit.isNegated() ? atom.notExpr() : atom; + expr_confl.push_back(expr_lit); + } + + Expr conflict = utils::mkSortedExpr(kind::OR, expr_confl); + Debug("pf::bv") << "Make conflict for " << conflict << std::endl; + + if (d_bbConflictMap.find(conflict) != d_bbConflictMap.end()) + { + Debug("pf::bv") << "Abort...already conflict for " << conflict << std::endl; + // This can only happen when we have eager explanations in the bv solver + // if we don't get to propagate p before ~p is already asserted + d_resolutionProof->cancelResChain(); + return; + } + + // we don't need to check for uniqueness in the sat solver then + ClauseId clause_id = d_resolutionProof->registerAssumptionConflict(confl); + d_bbConflictMap[conflict] = clause_id; + d_resolutionProof->endResChain(clause_id); + Debug("pf::bv") << "ResolutionBitVectorProof::endBVConflict id" << clause_id + << " => " << conflict << "\n"; + d_isAssumptionConflict = false; +} + +void ResolutionBitVectorProof::finalizeConflicts(std::vector<Expr>& conflicts) +{ + if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) + { + Debug("pf::bv") << "Construct full proof." << std::endl; + d_resolutionProof->constructProof(); + return; + } + + for (unsigned i = 0; i < conflicts.size(); ++i) + { + Expr confl = conflicts[i]; + Debug("pf::bv") << "Finalize conflict #" << i << ": " << confl << std::endl; + + // Special case: if the conflict has a (true) or a (not false) in it, it is + // trivial... + bool ignoreConflict = false; + if ((confl.isConst() && confl.getConst<bool>()) + || (confl.getKind() == kind::NOT && confl[0].isConst() + && !confl[0].getConst<bool>())) + { + ignoreConflict = true; + } + else if (confl.getKind() == kind::OR) + { + for (unsigned k = 0; k < confl.getNumChildren(); ++k) + { + if ((confl[k].isConst() && confl[k].getConst<bool>()) + || (confl[k].getKind() == kind::NOT && confl[k][0].isConst() + && !confl[k][0].getConst<bool>())) + { + ignoreConflict = true; + } + } + } + if (ignoreConflict) + { + Debug("pf::bv") << "Ignoring conflict due to (true) or (not false)" + << std::endl; + continue; + } + + if (d_bbConflictMap.find(confl) != d_bbConflictMap.end()) + { + ClauseId id = d_bbConflictMap[confl]; + d_resolutionProof->collectClauses(id); + } + else + { + // There is no exact match for our conflict, but maybe it is a subset of + // another conflict + ExprToClauseId::const_iterator it; + bool matchFound = false; + for (it = d_bbConflictMap.begin(); it != d_bbConflictMap.end(); ++it) + { + Expr possibleMatch = it->first; + if (possibleMatch.getKind() != kind::OR) + { + // This is a single-node conflict. If this node is in the conflict + // we're trying to prove, we have a match. + for (unsigned k = 0; k < confl.getNumChildren(); ++k) + { + if (confl[k] == possibleMatch) + { + matchFound = true; + d_resolutionProof->collectClauses(it->second); + break; + } + } + } + else + { + if (possibleMatch.getNumChildren() > confl.getNumChildren()) continue; + + unsigned k = 0; + bool matching = true; + for (unsigned j = 0; j < possibleMatch.getNumChildren(); ++j) + { + // j is the index in possibleMatch + // k is the index in confl + while (k < confl.getNumChildren() && confl[k] != possibleMatch[j]) + { + ++k; + } + if (k == confl.getNumChildren()) + { + // We couldn't find a match for possibleMatch[j], so not a match + matching = false; + break; + } + } + + if (matching) + { + Debug("pf::bv") + << "Collecting info from a sub-conflict" << std::endl; + d_resolutionProof->collectClauses(it->second); + matchFound = true; + break; + } + } + } + + if (!matchFound) + { + Debug("pf::bv") << "Do not collect clauses for " << confl << std::endl + << "Dumping existing conflicts:" << std::endl; + + i = 0; + for (it = d_bbConflictMap.begin(); it != d_bbConflictMap.end(); ++it) + { + ++i; + Debug("pf::bv") << "\tConflict #" << i << ": " << it->first + << std::endl; + } + + Unreachable(); + } + } + } +} + +void LFSCBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& lemma, + std::ostream& os, + std::ostream& paren, + const ProofLetMap& map) +{ + Debug("pf::bv") << "(pf::bv) LFSCBitVectorProof::printTheoryLemmaProof called" + << std::endl; + Expr conflict = utils::mkSortedExpr(kind::OR, lemma); + Debug("pf::bv") << "\tconflict = " << conflict << std::endl; + + if (d_bbConflictMap.find(conflict) != d_bbConflictMap.end()) + { + std::ostringstream lemma_paren; + for (unsigned i = 0; i < lemma.size(); ++i) + { + Expr lit = lemma[i]; + + if (lit.getKind() == kind::NOT) + { + os << "(intro_assump_t _ _ _ "; + } + else + { + os << "(intro_assump_f _ _ _ "; + } + lemma_paren << ")"; + // print corresponding literal in main sat solver + ProofManager* pm = ProofManager::currentPM(); + CnfProof* cnf = pm->getCnfProof(); + prop::SatLiteral main_lit = cnf->getLiteral(lit); + os << pm->getLitName(main_lit); + os << " "; + // print corresponding literal in bv sat solver + prop::SatVariable bb_var = d_cnfProof->getLiteral(lit).getSatVariable(); + os << pm->getAtomName(bb_var, "bb"); + os << "(\\ unit" << bb_var << "\n"; + lemma_paren << ")"; + } + Expr lem = utils::mkOr(lemma); + Assert(d_bbConflictMap.find(lem) != d_bbConflictMap.end()); + ClauseId lemma_id = d_bbConflictMap[lem]; + proof::LFSCProofPrinter::printAssumptionsResolution( + d_resolutionProof.get(), lemma_id, os, lemma_paren); + os << lemma_paren.str(); + } + else + { + Debug("pf::bv") << "Found a non-recorded conflict. Looking for a matching " + "sub-conflict..." + << std::endl; + + bool matching; + + ExprToClauseId::const_iterator it; + unsigned i = 0; + for (it = d_bbConflictMap.begin(); it != d_bbConflictMap.end(); ++it) + { + // Our conflict is sorted, and the records are also sorted. + ++i; + Expr possibleMatch = it->first; + + if (possibleMatch.getKind() != kind::OR) + { + // This is a single-node conflict. If this node is in the conflict we're + // trying to prove, we have a match. + matching = false; + + for (unsigned k = 0; k < conflict.getNumChildren(); ++k) + { + if (conflict[k] == possibleMatch) + { + matching = true; + break; + } + } + } + else + { + if (possibleMatch.getNumChildren() > conflict.getNumChildren()) + continue; + + unsigned k = 0; + + matching = true; + for (unsigned j = 0; j < possibleMatch.getNumChildren(); ++j) + { + // j is the index in possibleMatch + // k is the index in conflict + while (k < conflict.getNumChildren() + && conflict[k] != possibleMatch[j]) + { + ++k; + } + if (k == conflict.getNumChildren()) + { + // We couldn't find a match for possibleMatch[j], so not a match + matching = false; + break; + } + } + } + + if (matching) + { + Debug("pf::bv") << "Found a match with conflict #" << i << ": " + << std::endl + << possibleMatch << std::endl; + // The rest is just a copy of the usual handling, if a precise match is + // found. We only use the literals that appear in the matching conflict, + // though, and not in the original lemma - as these may not have even + // been bit blasted! + std::ostringstream lemma_paren; + + if (possibleMatch.getKind() == kind::OR) + { + for (unsigned i = 0; i < possibleMatch.getNumChildren(); ++i) + { + Expr lit = possibleMatch[i]; + + if (lit.getKind() == kind::NOT) + { + os << "(intro_assump_t _ _ _ "; + } + else + { + os << "(intro_assump_f _ _ _ "; + } + lemma_paren << ")"; + // print corresponding literal in main sat solver + ProofManager* pm = ProofManager::currentPM(); + CnfProof* cnf = pm->getCnfProof(); + prop::SatLiteral main_lit = cnf->getLiteral(lit); + os << pm->getLitName(main_lit); + os << " "; + // print corresponding literal in bv sat solver + prop::SatVariable bb_var = + d_cnfProof->getLiteral(lit).getSatVariable(); + os << pm->getAtomName(bb_var, "bb"); + os << "(\\ unit" << bb_var << "\n"; + lemma_paren << ")"; + } + } + else + { + // The conflict only consists of one node, either positive or + // negative. + Expr lit = possibleMatch; + if (lit.getKind() == kind::NOT) + { + os << "(intro_assump_t _ _ _ "; + } + else + { + os << "(intro_assump_f _ _ _ "; + } + lemma_paren << ")"; + // print corresponding literal in main sat solver + ProofManager* pm = ProofManager::currentPM(); + CnfProof* cnf = pm->getCnfProof(); + prop::SatLiteral main_lit = cnf->getLiteral(lit); + os << pm->getLitName(main_lit); + os << " "; + // print corresponding literal in bv sat solver + prop::SatVariable bb_var = + d_cnfProof->getLiteral(lit).getSatVariable(); + os << pm->getAtomName(bb_var, "bb"); + os << "(\\ unit" << bb_var << "\n"; + lemma_paren << ")"; + } + + ClauseId lemma_id = it->second; + proof::LFSCProofPrinter::printAssumptionsResolution( + d_resolutionProof.get(), lemma_id, os, lemma_paren); + os << lemma_paren.str(); + + return; + } + } + + // We failed to find a matching sub conflict. The last hope is that the + // conflict has a FALSE assertion in it; this can happen in some corner + // cases, where the FALSE is the result of a rewrite. + + for (unsigned i = 0; i < lemma.size(); ++i) + { + if (lemma[i].getKind() == kind::NOT && lemma[i][0] == utils::mkFalse()) + { + Debug("pf::bv") << "Lemma has a (not false) literal" << std::endl; + os << "(clausify_false "; + os << ProofManager::getLitName(lemma[i]); + os << ")"; + return; + } + } + + Debug("pf::bv") << "Failed to find a matching sub-conflict..." << std::endl + << "Dumping existing conflicts:" << std::endl; + + i = 0; + for (it = d_bbConflictMap.begin(); it != d_bbConflictMap.end(); ++it) + { + ++i; + Debug("pf::bv") << "\tConflict #" << i << ": " << it->first << std::endl; + } + + Unreachable(); + } +} + +void LFSCBitVectorProof::calculateAtomsInBitblastingProof() +{ + // Collect the input clauses used + IdToSatClause used_lemmas; + IdToSatClause used_inputs; + d_resolutionProof->collectClausesUsed(used_inputs, used_lemmas); + d_cnfProof->collectAtomsForClauses(used_inputs, d_atomsInBitblastingProof); + Assert(used_lemmas.empty()); +} + +void LFSCBitVectorProof::printResolutionProof(std::ostream& os, + std::ostream& paren, + ProofLetMap& letMap) +{ + // print mapping between theory atoms and internal SAT variables + os << std::endl << ";; BB atom mapping\n" << std::endl; + + std::set<Node>::iterator atomIt; + Debug("pf::bv") << std::endl + << "BV Dumping atoms from inputs: " << std::endl + << std::endl; + for (atomIt = d_atomsInBitblastingProof.begin(); + atomIt != d_atomsInBitblastingProof.end(); + ++atomIt) + { + Debug("pf::bv") << "\tAtom: " << *atomIt << std::endl; + } + Debug("pf::bv") << std::endl; + + // first print bit-blasting + printBitblasting(os, paren); + + // print CNF conversion proof for bit-blasted facts + IdToSatClause used_lemmas; + IdToSatClause used_inputs; + d_resolutionProof->collectClausesUsed(used_inputs, used_lemmas); + + d_cnfProof->printAtomMapping(d_atomsInBitblastingProof, os, paren, letMap); + os << std::endl << ";; Bit-blasting definitional clauses \n" << std::endl; + for (IdToSatClause::iterator it = used_inputs.begin(); + it != used_inputs.end(); + ++it) + { + d_cnfProof->printCnfProofForClause(it->first, it->second, os, paren); + } + + os << std::endl << " ;; Bit-blasting learned clauses \n" << std::endl; + proof::LFSCProofPrinter::printResolutions(d_resolutionProof.get(), os, paren); +} + +} /* namespace proof */ + +} /* namespace CVC4 */ diff --git a/src/proof/resolution_bitvector_proof.h b/src/proof/resolution_bitvector_proof.h new file mode 100644 index 000000000..ccb288f6e --- /dev/null +++ b/src/proof/resolution_bitvector_proof.h @@ -0,0 +1,133 @@ +/********************* */ +/*! \file resolution_bitvector_proof.h + ** \verbatim + ** Top contributors (to current version): + ** Liana Hadarean, Mathias Preiner, Guy Katz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Bitvector proof + ** + ** Bitvector proof + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PROOF__RESOLUTION_BITVECTOR_PROOF_H +#define __CVC4__PROOF__RESOLUTION_BITVECTOR_PROOF_H + +#include <iosfwd> + +#include "context/context.h" +#include "expr/expr.h" +#include "proof/bitvector_proof.h" +#include "proof/theory_proof.h" +#include "prop/bvminisat/core/Solver.h" + +namespace CVC4 { + +namespace theory { +namespace bv { +class TheoryBV; +template <class T> +class TBitblaster; +} // namespace bv +} // namespace theory + +// TODO(aozdemir) break the sat_solver - resolution_bitvectorproof - cnf_stream +// header cycle and remove this. +namespace prop { +class CnfStream; +} + +} /* namespace CVC4 */ + + +namespace CVC4 { + +template <class Solver> +class TSatProof; +typedef TSatProof<CVC4::BVMinisat::Solver> BVSatProof; + +namespace proof { + +/** + * Represents a bitvector proof which is backed by + * (a) bitblasting and + * (b) a resolution unsat proof. + * + * Contains tools for constructing BV conflicts + */ +class ResolutionBitVectorProof : public BitVectorProof +{ + public: + ResolutionBitVectorProof(theory::bv::TheoryBV* bv, + TheoryProofEngine* proofEngine); + + /** + * Create an (internal) SAT proof object + * Must be invoked before manipulating BV conflicts, + * or initializing a BNF proof + */ + void initSatProof(CVC4::BVMinisat::Solver* solver); + + BVSatProof* getSatProof(); + + /** + * Kind of a mess. + * In eager mode this must be invoked before printing a proof of the empty + * clause. In lazy mode the behavior is ??? + * TODO(aozdemir) clean this up. + */ + void finalizeConflicts(std::vector<Expr>& conflicts); + + void startBVConflict(CVC4::BVMinisat::Solver::TCRef cr); + void startBVConflict(CVC4::BVMinisat::Solver::TLit lit); + void endBVConflict(const BVMinisat::Solver::TLitVec& confl); + + void markAssumptionConflict() { d_isAssumptionConflict = true; } + bool isAssumptionConflict() const { return d_isAssumptionConflict; } + + virtual void printResolutionProof(std::ostream& os, + std::ostream& paren, + ProofLetMap& letMap) = 0; + + void initCnfProof(prop::CnfStream* cnfStream, context::Context* cnf) override; + + protected: + context::Context d_fakeContext; + + // The CNF formula that results from bit-blasting will need a proof. + // This is that proof. + std::unique_ptr<BVSatProof> d_resolutionProof; + + bool d_isAssumptionConflict; + + theory::TheoryId getTheoryId() override; +}; + +class LFSCBitVectorProof : public ResolutionBitVectorProof +{ + public: + LFSCBitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine) + : ResolutionBitVectorProof(bv, proofEngine) + { + } + void printTheoryLemmaProof(std::vector<Expr>& lemma, + std::ostream& os, + std::ostream& paren, + const ProofLetMap& map) override; + void printResolutionProof(std::ostream& os, + std::ostream& paren, + ProofLetMap& letMap) override; + void calculateAtomsInBitblastingProof() override; +}; + +} // namespace proof + +} // namespace CVC4 + +#endif /* __CVC4__PROOF__RESOLUTIONBITVECTORPROOF_H */ diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index cfad0a068..ee06fbfa0 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -22,12 +22,12 @@ #include "options/proof_options.h" #include "proof/arith_proof.h" #include "proof/array_proof.h" -#include "proof/bitvector_proof.h" #include "proof/clause_id.h" #include "proof/cnf_proof.h" #include "proof/proof_manager.h" #include "proof/proof_output_channel.h" #include "proof/proof_utils.h" +#include "proof/resolution_bitvector_proof.h" #include "proof/sat_proof.h" #include "proof/simplify_boolean_node.h" #include "proof/uf_proof.h" @@ -46,6 +46,9 @@ namespace CVC4 { +using proof::LFSCBitVectorProof; +using proof::ResolutionBitVectorProof; + unsigned CVC4::ProofLetCount::counter = 0; static unsigned LET_COUNT = 1; @@ -77,7 +80,8 @@ void TheoryProofEngine::registerTheory(theory::Theory* th) { } if (id == theory::THEORY_BV) { - BitVectorProof * bvp = new LFSCBitVectorProof((theory::bv::TheoryBV*)th, this); + auto bv_theory = static_cast<theory::bv::TheoryBV*>(th); + ResolutionBitVectorProof* bvp = new LFSCBitVectorProof(bv_theory, this); d_theoryProofTable[id] = bvp; return; } @@ -102,9 +106,9 @@ void TheoryProofEngine::finishRegisterTheory(theory::Theory* th) { theory::TheoryId id = th->getId(); if (id == theory::THEORY_BV) { Assert(d_theoryProofTable.find(id) != d_theoryProofTable.end()); - - BitVectorProof *bvp = (BitVectorProof *)d_theoryProofTable[id]; - ((theory::bv::TheoryBV*)th)->setProofLog( bvp ); + ResolutionBitVectorProof* bvp = + (ResolutionBitVectorProof*)d_theoryProofTable[id]; + ((theory::bv::TheoryBV*)th)->setResolutionProofLog(bvp); return; } } @@ -529,7 +533,7 @@ void LFSCTheoryProofEngine::finalizeBvConflicts(const IdToSatClause& lemmas, std } } - BitVectorProof* bv = ProofManager::getBitVectorProof(); + ResolutionBitVectorProof* bv = ProofManager::getBitVectorProof(); bv->finalizeConflicts(bv_lemmas); // bv->printResolutionProof(os, paren, letMap); } diff --git a/src/prop/bv_sat_solver_notify.h b/src/prop/bv_sat_solver_notify.h new file mode 100644 index 000000000..686848829 --- /dev/null +++ b/src/prop/bv_sat_solver_notify.h @@ -0,0 +1,49 @@ +/********************* */ +/*! \file sat_solver_notify.h + ** \verbatim + ** Top contributors (to current version): + ** Liana Hadarean, Dejan Jovanovic, Morgan Deters + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The interface for things that want to recieve notification from the + ** SAT solver + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PROP__BVSATSOLVERNOTIFY_H +#define __CVC4__PROP__BVSATSOLVERNOTIFY_H + +#include "prop/sat_solver_types.h" + +namespace CVC4 { +namespace prop { + +class BVSatSolverNotify { +public: + + virtual ~BVSatSolverNotify() {}; + + /** + * If the notify returns false, the solver will break out of whatever it's currently doing + * with an "unknown" answer. + */ + virtual bool notify(SatLiteral lit) = 0; + + /** + * Notify about a learnt clause. + */ + virtual void notify(SatClause& clause) = 0; + virtual void spendResource(unsigned amount) = 0; + virtual void safePoint(unsigned amount) = 0; + +};/* class BVSatSolverInterface::Notify */ + +} +} + +#endif diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp index 1eb4bce96..55710092b 100644 --- a/src/prop/bvminisat/bvminisat.cpp +++ b/src/prop/bvminisat/bvminisat.cpp @@ -51,7 +51,7 @@ void BVMinisatSatSolver::MinisatNotify::notify( d_notify->notify(satClause); } -void BVMinisatSatSolver::setNotify(Notify* notify) { +void BVMinisatSatSolver::setNotify(BVSatSolverNotify* notify) { d_minisatNotify.reset(new MinisatNotify(notify)); d_minisat->setNotify(d_minisatNotify.get()); } @@ -104,7 +104,8 @@ void BVMinisatSatSolver::popAssumption() { d_minisat->popAssumption(); } -void BVMinisatSatSolver::setProofLog( BitVectorProof * bvp ) { +void BVMinisatSatSolver::setProofLog(proof::ResolutionBitVectorProof* bvp) +{ d_minisat->setProofLog( bvp ); } diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h index 728d26bd4..16489b172 100644 --- a/src/prop/bvminisat/bvminisat.h +++ b/src/prop/bvminisat/bvminisat.h @@ -22,8 +22,10 @@ #include "context/cdo.h" #include "proof/clause_id.h" +#include "proof/resolution_bitvector_proof.h" #include "prop/bvminisat/simp/SimpSolver.h" #include "prop/sat_solver.h" +#include "prop/bv_sat_solver_notify.h" #include "util/statistics_registry.h" namespace CVC4 { @@ -35,10 +37,10 @@ class BVMinisatSatSolver : public BVSatSolverInterface, private: class MinisatNotify : public BVMinisat::Notify { - BVSatSolverInterface::Notify* d_notify; + BVSatSolverNotify* d_notify; public: - MinisatNotify(BVSatSolverInterface::Notify* notify) : d_notify(notify) {} + MinisatNotify(BVSatSolverNotify* notify) : d_notify(notify) {} bool notify(BVMinisat::Lit lit) override { return d_notify->notify(toSatLiteral(lit)); @@ -66,7 +68,7 @@ public: BVMinisatSatSolver(StatisticsRegistry* registry, context::Context* mainSatContext, const std::string& name = ""); virtual ~BVMinisatSatSolver(); - void setNotify(Notify* notify) override; + void setNotify(BVSatSolverNotify* notify) override; ClauseId addClause(SatClause& clause, bool removable) override; @@ -117,7 +119,7 @@ public: void popAssumption() override; - void setProofLog(BitVectorProof* bvp) override; + void setProofLog(proof::ResolutionBitVectorProof* bvp) override; private: /* Disable the default constructor. */ diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc index a4b0248e0..a877f20c3 100644 --- a/src/prop/bvminisat/core/Solver.cc +++ b/src/prop/bvminisat/core/Solver.cc @@ -29,9 +29,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "base/output.h" #include "options/bv_options.h" #include "options/smt_options.h" -#include "proof/bitvector_proof.h" #include "proof/clause_id.h" #include "proof/proof_manager.h" +#include "proof/resolution_bitvector_proof.h" #include "proof/sat_proof.h" #include "proof/sat_proof_implementation.h" #include "prop/bvminisat/mtl/Sort.h" @@ -1318,7 +1318,8 @@ void Solver::explain(Lit p, std::vector<Lit>& explanation) { } } -void Solver::setProofLog( BitVectorProof * bvp ) { +void Solver::setProofLog(proof::ResolutionBitVectorProof* bvp) +{ d_bvp = bvp; d_bvp->initSatProof(this); d_bvp->getSatProof()->registerTrueLit(mkLit(varTrue, false)); diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h index da4fb4c16..eef1c4e4c 100644 --- a/src/prop/bvminisat/core/Solver.h +++ b/src/prop/bvminisat/core/Solver.h @@ -39,7 +39,10 @@ namespace BVMinisat { class Solver; } -class BitVectorProof; +// TODO (aozdemir) replace this forward declaration with an include +namespace proof { +class ResolutionBitVectorProof; +} namespace BVMinisat { @@ -212,10 +215,10 @@ public: bool only_bcp; // solving mode in which only boolean constraint propagation is done void setOnlyBCP (bool val) { only_bcp = val;} void explain(Lit l, std::vector<Lit>& explanation); - - void setProofLog( CVC4::BitVectorProof * bvp ); -protected: + void setProofLog(CVC4::proof::ResolutionBitVectorProof* bvp); + + protected: // has a clause been added bool clause_added; @@ -292,7 +295,7 @@ protected: bool asynch_interrupt; //proof log - CVC4::BitVectorProof * d_bvp; + CVC4::proof::ResolutionBitVectorProof* d_bvp; // Main internal methods: // diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index 5222af200..49064c20f 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -26,13 +26,13 @@ #include "context/cdlist.h" #include "context/context.h" #include "expr/node.h" +#include "proof/resolution_bitvector_proof.h" #include "proof/clause_id.h" #include "prop/sat_solver_types.h" +#include "prop/bv_sat_solver_notify.h" #include "util/statistics_registry.h" namespace CVC4 { - -class BitVectorProof; namespace prop { @@ -96,9 +96,9 @@ public: /** Check if the solver is in an inconsistent state */ virtual bool ok() const = 0; - - virtual void setProofLog( BitVectorProof * bvp ) {} - + + virtual void setProofLog(proof::ResolutionBitVectorProof* bvp) {} + };/* class SatSolver */ @@ -107,27 +107,8 @@ public: virtual ~BVSatSolverInterface() {} /** Interface for notifications */ - class Notify { - public: - - virtual ~Notify() {}; - - /** - * If the notify returns false, the solver will break out of whatever it's currently doing - * with an "unknown" answer. - */ - virtual bool notify(SatLiteral lit) = 0; - - /** - * Notify about a learnt clause. - */ - virtual void notify(SatClause& clause) = 0; - virtual void spendResource(unsigned amount) = 0; - virtual void safePoint(unsigned amount) = 0; - - };/* class BVSatSolverInterface::Notify */ - virtual void setNotify(Notify* notify) = 0; + virtual void setNotify(BVSatSolverNotify* notify) = 0; virtual void markUnremovable(SatLiteral lit) = 0; diff --git a/src/prop/sat_solver_types.h b/src/prop/sat_solver_types.h index f041f6898..ed1c5397d 100644 --- a/src/prop/sat_solver_types.h +++ b/src/prop/sat_solver_types.h @@ -24,8 +24,9 @@ #include "cvc4_private.h" -#include <string> #include <sstream> +#include <string> +#include <vector> namespace CVC4 { namespace prop { diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index a0939f4db..ae20fa156 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1071,6 +1071,18 @@ SmtEngine::~SmtEngine() //destroy all passes before destroying things that they refer to d_private->cleanupPreprocessingPasses(); + // d_proofManager is always created when proofs are enabled at configure + // time. Because of this, this code should not be wrapped in PROOF() which + // additionally checks flags such as options::proof(). + // + // Note: the proof manager must be destroyed before the theory engine. + // Because the destruction of the proofs depends on contexts owned be the + // theory solvers. +#ifdef CVC4_PROOF + delete d_proofManager; + d_proofManager = NULL; +#endif + delete d_theoryEngine; d_theoryEngine = NULL; delete d_propEngine; @@ -1078,15 +1090,6 @@ SmtEngine::~SmtEngine() delete d_decisionEngine; d_decisionEngine = NULL; - -// d_proofManager is always created when proofs are enabled at configure time. -// Becuase of this, this code should not be wrapped in PROOF() which -// additionally checks flags such as options::proof(). -#ifdef CVC4_PROOF - delete d_proofManager; - d_proofManager = NULL; -#endif - delete d_stats; d_stats = NULL; delete d_statisticsRegistry; @@ -1376,17 +1379,17 @@ void SmtEngine::setDefaults() { options::bitvectorToBool.set(false); } - if (options::boolToBitvector()) + if (options::boolToBitvector() != preprocessing::passes::BOOL_TO_BV_OFF) { if (options::boolToBitvector.wasSetByUser()) { throw OptionException( - "bool-to-bv not supported with unsat cores/proofs"); + "bool-to-bv != off not supported with unsat cores/proofs"); } - Notice() << "SmtEngine: turning off bool-to-bitvector to support unsat " + Notice() << "SmtEngine: turning off bool-to-bv to support unsat " "cores/proofs" << endl; - options::boolToBitvector.set(false); + setOption("boolToBitvector", SExpr("off")); } if (options::bvIntroducePow2()) @@ -1446,13 +1449,18 @@ void SmtEngine::setDefaults() { if (options::cbqiBv() && d_logic.isQuantified()) { - if(options::boolToBitvector.wasSetByUser()) { - throw OptionException( - "bool-to-bv not supported with CBQI BV for quantified logics"); + if (options::boolToBitvector() != preprocessing::passes::BOOL_TO_BV_OFF) + { + if (options::boolToBitvector.wasSetByUser()) + { + throw OptionException( + "bool-to-bv != off not supported with CBQI BV for quantified " + "logics"); + } + Notice() << "SmtEngine: turning off bool-to-bitvector to support CBQI BV" + << endl; + setOption("boolToBitvector", SExpr("off")); } - Notice() << "SmtEngine: turning off bool-to-bitvector to support CBQI BV" - << endl; - options::boolToBitvector.set(false); } // cases where we need produce models @@ -1614,6 +1622,19 @@ void SmtEngine::setDefaults() { } } + if (options::boolToBitvector() == preprocessing::passes::BOOL_TO_BV_ALL + && !d_logic.isTheoryEnabled(THEORY_BV)) + { + if (options::boolToBitvector.wasSetByUser()) + { + throw OptionException( + "bool-to-bv=all not supported for non-bitvector logics."); + } + Notice() << "SmtEngine: turning off bool-to-bv for non-bv logic: " + << d_logic.getLogicString() << std::endl; + setOption("boolToBitvector", SExpr("off")); + } + if (! options::bvEagerExplanations.wasSetByUser() && d_logic.isTheoryEnabled(THEORY_ARRAYS) && d_logic.isTheoryEnabled(THEORY_BV)) { @@ -1788,12 +1809,6 @@ void SmtEngine::setDefaults() { options::mbqiMode.set( quantifiers::MBQI_NONE ); } } - if( options::mbqiMode()==quantifiers::MBQI_ABS ){ - if( !d_logic.isPure(THEORY_UF) ){ - //MBQI_ABS is only supported in pure quantified UF - options::mbqiMode.set( quantifiers::MBQI_FMC ); - } - } if( options::fmfFunWellDefinedRelevant() ){ if( !options::fmfFunWellDefined.wasSetByUser() ){ options::fmfFunWellDefined.set( true ); @@ -1831,17 +1846,6 @@ void SmtEngine::setDefaults() { options::instWhenMode.set( quantifiers::INST_WHEN_LAST_CALL ); } } - if( options::mbqiMode()==quantifiers::MBQI_ABS ){ - if( !options::preSkolemQuant.wasSetByUser() ){ - options::preSkolemQuant.set( true ); - } - if( !options::preSkolemQuantNested.wasSetByUser() ){ - options::preSkolemQuantNested.set( true ); - } - if( !options::fmfOneInstPerRound.wasSetByUser() ){ - options::fmfOneInstPerRound.set( true ); - } - } } //apply counterexample guided instantiation options diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index ff71f6432..352ba0f36 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -602,7 +602,7 @@ void ConstraintRule::print(std::ostream& out) const { bool Constraint::wellFormedFarkasProof() const { Assert(hasProof()); - + const ConstraintRule& cr = getConstraintRule(); if(cr.d_constraint != this){ return false; } if(cr.d_proofType != FarkasAP){ return false; } @@ -1071,6 +1071,7 @@ ConstraintP ConstraintDatabase::lookup(TNode literal) const{ } void Constraint::setAssumption(bool nowInConflict){ + Debug("constraints::pf") << "setAssumption(" << this << ")" << std::endl; Assert(!hasProof()); Assert(negationHasProof() == nowInConflict); Assert(hasLiteral()); @@ -1113,6 +1114,7 @@ void Constraint::propagate(){ * 1*(x <= a) + (-1)*(x > b) => (0 <= a-b) */ void Constraint::impliedByUnate(ConstraintCP imp, bool nowInConflict){ + Debug("constraints::pf") << "impliedByUnate(" << this << ", " << *imp << ")" << std::endl; Assert(!hasProof()); Assert(imp->hasProof()); Assert(negationHasProof() == nowInConflict); @@ -1152,6 +1154,8 @@ void Constraint::impliedByUnate(ConstraintCP imp, bool nowInConflict){ } void Constraint::impliedByTrichotomy(ConstraintCP a, ConstraintCP b, bool nowInConflict){ + Debug("constraints::pf") << "impliedByTrichotomy(" << this << ", " << *a << ", "; + Debug("constraints::pf") << *b << ")" << std::endl; Assert(!hasProof()); Assert(negationHasProof() == nowInConflict); Assert(a->hasProof()); @@ -1180,6 +1184,7 @@ bool Constraint::allHaveProof(const ConstraintCPVec& b){ } void Constraint::impliedByIntHole(ConstraintCP a, bool nowInConflict){ + Debug("constraints::pf") << "impliedByIntHole(" << this << ", " << *a << ")" << std::endl; Assert(!hasProof()); Assert(negationHasProof() == nowInConflict); Assert(a->hasProof()); @@ -1196,6 +1201,15 @@ void Constraint::impliedByIntHole(ConstraintCP a, bool nowInConflict){ } void Constraint::impliedByIntHole(const ConstraintCPVec& b, bool nowInConflict){ + Debug("constraints::pf") << "impliedByIntHole(" << this; + if (Debug.isOn("constraints::pf")) { + for (const ConstraintCP& p : b) + { + Debug("constraints::pf") << ", " << p; + } + } + Debug("constraints::pf") << ")" << std::endl; + Assert(!hasProof()); Assert(negationHasProof() == nowInConflict); Assert(allHaveProof(b)); @@ -1224,6 +1238,15 @@ void Constraint::impliedByIntHole(const ConstraintCPVec& b, bool nowInConflict){ * coeff.back() corresponds to the current constraint. */ void Constraint::impliedByFarkas(const ConstraintCPVec& a, RationalVectorCP coeffs, bool nowInConflict){ + Debug("constraints::pf") << "impliedByFarkas(" << this; + if (Debug.isOn("constraints::pf")) { + for (const ConstraintCP& p : a) + { + Debug("constraints::pf") << ", " << p; + } + } + Debug("constraints::pf") << ", <coeffs>"; + Debug("constraints::pf") << ")" << std::endl; Assert(!hasProof()); Assert(negationHasProof() == nowInConflict); Assert(allHaveProof(a)); @@ -1263,6 +1286,8 @@ void Constraint::impliedByFarkas(const ConstraintCPVec& a, RationalVectorCP coef void Constraint::setInternalAssumption(bool nowInConflict){ + Debug("constraints::pf") << "setInternalAssumption(" << this; + Debug("constraints::pf") << ")" << std::endl; Assert(!hasProof()); Assert(negationHasProof() == nowInConflict); Assert(!assertedToTheTheory()); @@ -1277,6 +1302,8 @@ void Constraint::setInternalAssumption(bool nowInConflict){ void Constraint::setEqualityEngineProof(){ + Debug("constraints::pf") << "setEqualityEngineProof(" << this; + Debug("constraints::pf") << ")" << std::endl; Assert(truthIsUnknown()); Assert(hasLiteral()); d_database->pushConstraintRule(ConstraintRule(this, EqualityEngineAP)); diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index 5eef9663e..d411f2d34 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -928,7 +928,11 @@ private: /** Return true if every element in b has a proof. */ static bool allHaveProof(const ConstraintCPVec& b); - /** Precondition: hasFarkasProof() */ + /** Precondition: hasFarkasProof() + * Computes the combination implied by the farkas coefficients. Sees if it is + * a contradiction. + */ + bool wellFormedFarkasProof() const; }; /* class ConstraintValue */ diff --git a/src/theory/arith/cut_log.h b/src/theory/arith/cut_log.h index 6650e6680..5fd585588 100644 --- a/src/theory/arith/cut_log.h +++ b/src/theory/arith/cut_log.h @@ -216,7 +216,7 @@ public: int getUpId() const; /** - * Looks up a row id to the appropraite arith variable. + * Looks up a row id to the appropriate arith variable. * Be careful these are deleted in context during replay! * failure returns ARITHVAR_SENTINEL */ ArithVar lookupRowId(int rowId) const; diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index d7113b17d..9902121d0 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -36,6 +36,7 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo) , d_internal(new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo)) , d_ppRewriteTimer("theory::arith::ppRewriteTimer") + , d_proofRecorder(nullptr) { smtStatisticsRegistry()->registerStat(&d_ppRewriteTimer); if (options::nlExt()) { diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 195cb1883..e4b1c5b26 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -19,6 +19,7 @@ #include "theory/theory.h" #include "expr/node.h" +#include "proof/arith_proof_recorder.h" #include "theory/arith/theory_arith_private_forward.h" @@ -40,6 +41,11 @@ private: TimerStat d_ppRewriteTimer; + /** + * @brief Where to store Farkas proofs of lemmas + */ + proof::ArithProofRecorder * d_proofRecorder; + public: TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); @@ -90,6 +96,11 @@ public: const EntailmentCheckParameters* params, EntailmentCheckSideEffects* out) override; + void setProofRecorder(proof::ArithProofRecorder * proofRecorder) + { + d_proofRecorder = proofRecorder; + } + };/* class TheoryArith */ }/* CVC4::theory::arith namespace */ diff --git a/src/theory/bv/bitblast/aig_bitblaster.h b/src/theory/bv/bitblast/aig_bitblaster.h index 6d21b69e6..62e70d73d 100644 --- a/src/theory/bv/bitblast/aig_bitblaster.h +++ b/src/theory/bv/bitblast/aig_bitblaster.h @@ -20,6 +20,7 @@ #define __CVC4__THEORY__BV__BITBLAST__AIG_BITBLASTER_H #include "theory/bv/bitblast/bitblaster.h" +#include "prop/sat_solver.h" class Abc_Obj_t_; typedef Abc_Obj_t_ Abc_Obj_t; diff --git a/src/theory/bv/bitblast/bitblaster.h b/src/theory/bv/bitblast/bitblaster.h index 9e2dac2f3..73b4d19c7 100644 --- a/src/theory/bv/bitblast/bitblaster.h +++ b/src/theory/bv/bitblast/bitblaster.h @@ -24,7 +24,8 @@ #include <vector> #include "expr/node.h" -#include "prop/sat_solver.h" +#include "prop/bv_sat_solver_notify.h" +#include "prop/sat_solver_types.h" #include "theory/bv/bitblast/bitblast_strategies_template.h" #include "theory/theory_registrar.h" #include "theory/valuation.h" @@ -59,8 +60,6 @@ class TBitblaster TermDefMap d_termCache; ModelCache d_modelCache; - BitVectorProof* d_bvp; - void initAtomBBStrategies(); void initTermBBStrategies(); @@ -94,7 +93,7 @@ class TBitblaster void invalidateModelCache(); }; -class MinisatEmptyNotify : public prop::BVSatSolverInterface::Notify +class MinisatEmptyNotify : public prop::BVSatSolverNotify { public: MinisatEmptyNotify() {} @@ -172,7 +171,7 @@ void TBitblaster<T>::initTermBBStrategies() } template <class T> -TBitblaster<T>::TBitblaster() : d_termCache(), d_modelCache(), d_bvp(NULL) +TBitblaster<T>::TBitblaster() : d_termCache(), d_modelCache() { initAtomBBStrategies(); initTermBBStrategies(); diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp index 01437cb64..019918c2f 100644 --- a/src/theory/bv/bitblast/eager_bitblaster.cpp +++ b/src/theory/bv/bitblast/eager_bitblaster.cpp @@ -19,7 +19,6 @@ #include "theory/bv/bitblast/eager_bitblaster.h" #include "options/bv_options.h" -#include "proof/bitvector_proof.h" #include "prop/cnf_stream.h" #include "prop/sat_solver_factory.h" #include "smt/smt_statistics_registry.h" @@ -37,6 +36,7 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv, context::Context* c) d_satSolver(), d_bitblastingRegistrar(new BitblastingRegistrar(this)), d_cnfStream(), + d_bvp(nullptr), d_bv(theory_bv), d_bbAtoms(), d_variables(), @@ -99,8 +99,8 @@ void EagerBitblaster::bbFormula(TNode node) void EagerBitblaster::bbAtom(TNode node) { node = node.getKind() == kind::NOT ? node[0] : node; - if (node.getKind() == kind::BITVECTOR_BITOF) return; - if (hasBBAtom(node)) + if (node.getKind() == kind::BITVECTOR_BITOF + || node.getKind() == kind::CONST_BOOLEAN || hasBBAtom(node)) { return; } @@ -268,10 +268,11 @@ bool EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) return true; } -void EagerBitblaster::setProofLog(BitVectorProof* bvp) { - d_bvp = bvp; - d_satSolver->setProofLog(bvp); - bvp->initCnfProof(d_cnfStream.get(), d_nullContext.get()); +void EagerBitblaster::setResolutionProofLog( + proof::ResolutionBitVectorProof* bvp) +{ + THEORY_PROOF(d_bvp = bvp; d_satSolver->setProofLog(bvp); + bvp->initCnfProof(d_cnfStream.get(), d_nullContext.get());) } bool EagerBitblaster::isSharedTerm(TNode node) { diff --git a/src/theory/bv/bitblast/eager_bitblaster.h b/src/theory/bv/bitblast/eager_bitblaster.h index 3e6190d76..3299ffc54 100644 --- a/src/theory/bv/bitblast/eager_bitblaster.h +++ b/src/theory/bv/bitblast/eager_bitblaster.h @@ -23,6 +23,8 @@ #include "theory/bv/bitblast/bitblaster.h" +#include "proof/bitvector_proof.h" +#include "proof/resolution_bitvector_proof.h" #include "prop/cnf_stream.h" #include "prop/sat_solver.h" @@ -53,7 +55,7 @@ class EagerBitblaster : public TBitblaster<Node> bool solve(); bool solve(const std::vector<Node>& assumptions); bool collectModelInfo(TheoryModel* m, bool fullModel); - void setProofLog(BitVectorProof* bvp); + void setResolutionProofLog(proof::ResolutionBitVectorProof* bvp); private: context::Context* d_context; @@ -65,6 +67,8 @@ class EagerBitblaster : public TBitblaster<Node> std::unique_ptr<BitblastingRegistrar> d_bitblastingRegistrar; std::unique_ptr<prop::CnfStream> d_cnfStream; + BitVectorProof* d_bvp; + TheoryBV* d_bv; TNodeSet d_bbAtoms; TNodeSet d_variables; diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp index a50916413..529f0373b 100644 --- a/src/theory/bv/bitblast/lazy_bitblaster.cpp +++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp @@ -19,17 +19,16 @@ #include "theory/bv/bitblast/lazy_bitblaster.h" #include "options/bv_options.h" +#include "proof/proof_manager.h" #include "prop/cnf_stream.h" #include "prop/sat_solver.h" #include "prop/sat_solver_factory.h" #include "smt/smt_statistics_registry.h" #include "theory/bv/abstraction.h" #include "theory/bv/theory_bv.h" +#include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" #include "theory/theory_model.h" -#include "proof/bitvector_proof.h" -#include "proof/proof_manager.h" -#include "theory/bv/theory_bv_utils.h" namespace CVC4 { namespace theory { @@ -65,6 +64,7 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c, bool emptyNotify) : TBitblaster<Node>(), d_bv(bv), + d_bvp(nullptr), d_ctx(c), d_nullRegistrar(new prop::NullRegistrar()), d_nullContext(new context::Context()), @@ -90,8 +90,8 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c, d_satSolverNotify.reset( d_emptyNotify - ? (prop::BVSatSolverInterface::Notify*)new MinisatEmptyNotify() - : (prop::BVSatSolverInterface::Notify*)new MinisatNotify( + ? (prop::BVSatSolverNotify*)new MinisatEmptyNotify() + : (prop::BVSatSolverNotify*)new MinisatNotify( d_cnfStream.get(), bv, this)); d_satSolver->setNotify(d_satSolverNotify.get()); @@ -566,7 +566,8 @@ bool TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) return true; } -void TLazyBitblaster::setProofLog( BitVectorProof * bvp ){ +void TLazyBitblaster::setProofLog(proof::ResolutionBitVectorProof* bvp) +{ d_bvp = bvp; d_satSolver->setProofLog( bvp ); bvp->initCnfProof(d_cnfStream.get(), d_nullContext.get()); @@ -590,8 +591,8 @@ void TLazyBitblaster::clearSolver() { d_satSolver.get(), d_nullRegistrar.get(), d_nullContext.get())); d_satSolverNotify.reset( d_emptyNotify - ? (prop::BVSatSolverInterface::Notify*)new MinisatEmptyNotify() - : (prop::BVSatSolverInterface::Notify*)new MinisatNotify( + ? (prop::BVSatSolverNotify*)new MinisatEmptyNotify() + : (prop::BVSatSolverNotify*)new MinisatNotify( d_cnfStream.get(), d_bv, this)); d_satSolver->setNotify(d_satSolverNotify.get()); } diff --git a/src/theory/bv/bitblast/lazy_bitblaster.h b/src/theory/bv/bitblast/lazy_bitblaster.h index 5e16b743a..1195d3590 100644 --- a/src/theory/bv/bitblast/lazy_bitblaster.h +++ b/src/theory/bv/bitblast/lazy_bitblaster.h @@ -19,13 +19,14 @@ #ifndef __CVC4__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H #define __CVC4__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H +#include "proof/resolution_bitvector_proof.h" #include "theory/bv/bitblast/bitblaster.h" #include "context/cdhashmap.h" #include "context/cdlist.h" #include "prop/cnf_stream.h" #include "prop/registrar.h" -#include "prop/sat_solver.h" +#include "prop/bv_sat_solver_notify.h" #include "theory/bv/abstraction.h" namespace CVC4 { @@ -76,7 +77,7 @@ class TLazyBitblaster : public TBitblaster<Node> * constants to equivalence classes that don't already have them */ bool collectModelInfo(TheoryModel* m, bool fullModel); - void setProofLog(BitVectorProof* bvp); + void setProofLog(proof::ResolutionBitVectorProof* bvp); typedef TNodeSet::const_iterator vars_iterator; vars_iterator beginVars() { return d_variables.begin(); } @@ -106,7 +107,7 @@ class TLazyBitblaster : public TBitblaster<Node> prop::SatLiteralHashFunction> ExplanationMap; /** This class gets callbacks from minisat on propagations */ - class MinisatNotify : public prop::BVSatSolverInterface::Notify + class MinisatNotify : public prop::BVSatSolverNotify { prop::CnfStream* d_cnf; TheoryBV* d_bv; @@ -125,13 +126,14 @@ class TLazyBitblaster : public TBitblaster<Node> }; TheoryBV* d_bv; + proof::ResolutionBitVectorProof* d_bvp; context::Context* d_ctx; std::unique_ptr<prop::NullRegistrar> d_nullRegistrar; std::unique_ptr<context::Context> d_nullContext; // sat solver used for bitblasting and associated CnfStream std::unique_ptr<prop::BVSatSolverInterface> d_satSolver; - std::unique_ptr<prop::BVSatSolverInterface::Notify> d_satSolverNotify; + std::unique_ptr<prop::BVSatSolverNotify> d_satSolverNotify; std::unique_ptr<prop::CnfStream> d_cnfStream; AssertionList* diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp index 27a48875d..119195c4a 100644 --- a/src/theory/bv/bv_eager_solver.cpp +++ b/src/theory/bv/bv_eager_solver.cpp @@ -17,7 +17,6 @@ #include "theory/bv/bv_eager_solver.h" #include "options/bv_options.h" -#include "proof/bitvector_proof.h" #include "theory/bv/bitblast/aig_bitblaster.h" #include "theory/bv/bitblast/eager_bitblaster.h" @@ -57,7 +56,7 @@ void EagerBitblastSolver::initialize() { } else { d_bitblaster.reset(new EagerBitblaster(d_bv, d_context)); THEORY_PROOF(if (d_bvp) { - d_bitblaster->setProofLog(d_bvp); + d_bitblaster->setResolutionProofLog(d_bvp); d_bvp->setBitblaster(d_bitblaster.get()); }); } @@ -128,7 +127,11 @@ bool EagerBitblastSolver::collectModelInfo(TheoryModel* m, bool fullModel) return d_bitblaster->collectModelInfo(m, fullModel); } -void EagerBitblastSolver::setProofLog(BitVectorProof* bvp) { d_bvp = bvp; } +void EagerBitblastSolver::setResolutionProofLog( + proof::ResolutionBitVectorProof* bvp) +{ + d_bvp = bvp; +} } // namespace bv } // namespace theory diff --git a/src/theory/bv/bv_eager_solver.h b/src/theory/bv/bv_eager_solver.h index b17cd6ebc..7f688b3ae 100644 --- a/src/theory/bv/bv_eager_solver.h +++ b/src/theory/bv/bv_eager_solver.h @@ -23,6 +23,7 @@ #include <vector> #include "expr/node.h" +#include "proof/resolution_bitvector_proof.h" #include "theory/bv/theory_bv.h" #include "theory/theory_model.h" @@ -47,7 +48,7 @@ class EagerBitblastSolver { bool isInitialized(); void initialize(); bool collectModelInfo(theory::TheoryModel* m, bool fullModel); - void setProofLog(BitVectorProof* bvp); + void setResolutionProofLog(proof::ResolutionBitVectorProof* bvp); private: context::CDHashSet<Node, NodeHashFunction> d_assertionSet; @@ -60,7 +61,7 @@ class EagerBitblastSolver { bool d_useAig; TheoryBV* d_bv; - BitVectorProof* d_bvp; + proof::ResolutionBitVectorProof* d_bvp; }; // class EagerBitblastSolver } // namespace bv diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h index 3166401aa..31c542e0b 100644 --- a/src/theory/bv/bv_subtheory.h +++ b/src/theory/bv/bv_subtheory.h @@ -24,6 +24,11 @@ #include "theory/theory.h" namespace CVC4 { + +namespace proof { +class ResolutionBitVectorProof; +} + namespace theory { class TheoryModel; @@ -88,7 +93,7 @@ class SubtheorySolver { return res; } virtual void assertFact(TNode fact) { d_assertionQueue.push_back(fact); } - virtual void setProofLog(BitVectorProof* bvp) {} + virtual void setProofLog(proof::ResolutionBitVectorProof* bvp) {} AssertionQueue::const_iterator assertionsBegin() { return d_assertionQueue.begin(); } @@ -103,7 +108,7 @@ class SubtheorySolver { /** The bit-vector theory */ TheoryBV* d_bv; /** proof log */ - BitVectorProof* d_bvp; + proof::ResolutionBitVectorProof* d_bvp; AssertionQueue d_assertionQueue; context::CDO<uint32_t> d_assertionIndex; }; /* class SubtheorySolver */ diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp index ea2f8e4bf..ff9dd52c2 100644 --- a/src/theory/bv/bv_subtheory_bitblast.cpp +++ b/src/theory/bv/bv_subtheory_bitblast.cpp @@ -18,7 +18,6 @@ #include "decision/decision_attributes.h" #include "options/bv_options.h" #include "options/decision_options.h" -#include "proof/bitvector_proof.h" #include "proof/proof_manager.h" #include "smt/smt_statistics_registry.h" #include "theory/bv/abstraction.h" @@ -277,7 +276,8 @@ void BitblastSolver::setConflict(TNode conflict) { d_bv->setConflict(final_conflict); } -void BitblastSolver::setProofLog( BitVectorProof * bvp ) { +void BitblastSolver::setProofLog(proof::ResolutionBitVectorProof* bvp) +{ d_bitblaster->setProofLog( bvp ); bvp->setBitblaster(d_bitblaster.get()); } diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h index ac0d38815..aa2c90c43 100644 --- a/src/theory/bv/bv_subtheory_bitblast.h +++ b/src/theory/bv/bv_subtheory_bitblast.h @@ -23,6 +23,11 @@ #include "theory/bv/bv_subtheory.h" namespace CVC4 { + +namespace proof { +class ResolutionBitVectorProof; +} + namespace theory { namespace bv { @@ -74,7 +79,7 @@ public: void bitblastQueue(); void setAbstraction(AbstractionModule* module); uint64_t computeAtomWeight(TNode atom); - void setProofLog(BitVectorProof* bvp) override; + void setProofLog(proof::ResolutionBitVectorProof* bvp) override; }; } /* namespace CVC4::theory::bv */ diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index d08405ef3..949a3d738 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -740,7 +740,7 @@ Node TheoryBV::ppRewrite(TNode t) { Debug("bv-pp-rewrite") << "TheoryBV::ppRewrite " << t << "\n"; Node res = t; - if (RewriteRule<BitwiseEq>::applies(t)) { + if (options::bitwiseEq() && RewriteRule<BitwiseEq>::applies(t)) { Node result = RewriteRule<BitwiseEq>::run<false>(t); res = Rewriter::rewrite(result); } else if (d_isCoreTheory && t.getKind() == kind::EQUAL) { @@ -986,9 +986,10 @@ bool TheoryBV::applyAbstraction(const std::vector<Node>& assertions, std::vector return changed; } -void TheoryBV::setProofLog( BitVectorProof * bvp ) { +void TheoryBV::setResolutionProofLog(proof::ResolutionBitVectorProof* bvp) +{ if( options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER ){ - d_eagerSolver->setProofLog( bvp ); + d_eagerSolver->setResolutionProofLog(bvp); }else{ for( unsigned i=0; i< d_subtheories.size(); i++ ){ d_subtheories[i]->setProofLog( bvp ); diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index d5e3ad02e..afa9f4b4f 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -104,9 +104,9 @@ public: bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions); - void setProofLog( BitVectorProof * bvp ); + void setResolutionProofLog(proof::ResolutionBitVectorProof* bvp); -private: + private: class Statistics { public: diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index 7efdc2c81..c58d69f6f 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -535,7 +535,7 @@ inline Node RewriteRule<AndOrXorConcatPullUp>::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule<AndOrXorConcatPullUp>(" << node << ")" << std::endl; - uint32_t m, my, mz, n; + uint32_t m, my, mz; size_t nc; Kind kind = node.getKind(); TNode concat; @@ -589,7 +589,9 @@ inline Node RewriteRule<AndOrXorConcatPullUp>::apply(TNode node) z = nc > 1 ? zb.constructNode() : zb[0]; } m = utils::getSize(x); - n = utils::getSize(c); +#ifdef CVC4_ASSERTIONS + uint32_t n = utils::getSize(c); +#endif my = y.isNull() ? 0 : utils::getSize(y); mz = z.isNull() ? 0 : utils::getSize(z); Assert(mz == m - my - n); diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp index b583a55da..ae053930c 100644 --- a/src/theory/quantifiers/extended_rewrite.cpp +++ b/src/theory/quantifiers/extended_rewrite.cpp @@ -119,7 +119,8 @@ Node ExtendedRewriter::extendedRewrite(Node n) Kind k = n.getKind(); bool childChanged = false; bool isNonAdditive = TermUtil::isNonAdditive(k); - bool isAssoc = TermUtil::isAssoc(k); + // We flatten associative operators below, which requires k to be n-ary. + bool isAssoc = TermUtil::isAssoc(k, true); for (unsigned i = 0; i < n.getNumChildren(); i++) { Node nc = extendedRewrite(n[i]); diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 0eec40de2..5eb65ed21 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -15,7 +15,6 @@ #include "theory/quantifiers/first_order_model.h" #include "options/base_options.h" #include "options/quantifiers_options.h" -#include "theory/quantifiers/fmf/ambqi_builder.h" #include "theory/quantifiers/fmf/bounded_integers.h" #include "theory/quantifiers/fmf/full_model_check.h" #include "theory/quantifiers/fmf/model_engine.h" @@ -414,473 +413,6 @@ unsigned FirstOrderModel::getModelBasisArg(Node n) return n.getAttribute(ModelBasisArgAttribute()); } -Node FirstOrderModelIG::UfModelTreeGenerator::getIntersection(TheoryModel* m, - Node n1, - Node n2, - bool& isGround) -{ - isGround = true; - std::vector<Node> children; - children.push_back(n1.getOperator()); - for (unsigned i = 0, size = n1.getNumChildren(); i < size; i++) - { - if (n1[i] == n2[i]) - { - if (n1[i].getAttribute(ModelBasisAttribute())) - { - isGround = false; - } - children.push_back(n1[i]); - } - else if (n1[i].getAttribute(ModelBasisAttribute())) - { - children.push_back(n2[i]); - } - else if (n2[i].getAttribute(ModelBasisAttribute())) - { - children.push_back(n1[i]); - } - else if (m->areEqual(n1[i], n2[i])) - { - children.push_back(n1[i]); - } - else - { - return Node::null(); - } - } - return NodeManager::currentNM()->mkNode(APPLY_UF, children); -} - -void FirstOrderModelIG::UfModelTreeGenerator::setValue( - TheoryModel* m, Node n, Node v, bool ground, bool isReq) -{ - Assert(!n.isNull()); - Assert(!v.isNull()); - d_set_values[isReq ? 1 : 0][ground ? 1 : 0][n] = v; - if (!ground) - { - for (unsigned i = 0, defSize = d_defaults.size(); i < defSize; i++) - { - // for correctness, to allow variable order-independent function - // interpretations, we must ensure that the intersection of all default - // terms is also defined. - // for example, if we have that f( e, a ) = ..., and f( b, e ) = ..., - // then we must define f( b, a ). - bool isGround; - Node ni = getIntersection(m, n, d_defaults[i], isGround); - if (!ni.isNull()) - { - // if the intersection exists, and is not already defined - if (d_set_values[0][isGround ? 1 : 0].find(ni) - == d_set_values[0][isGround ? 1 : 0].end() - && d_set_values[1][isGround ? 1 : 0].find(ni) - == d_set_values[1][isGround ? 1 : 0].end()) - { - // use the current value - setValue(m, ni, v, isGround, false); - } - } - } - d_defaults.push_back(n); - } - if (isReq - && d_set_values[0][ground ? 1 : 0].find(n) - != d_set_values[0][ground ? 1 : 0].end()) - { - d_set_values[0][ground ? 1 : 0].erase(n); - } -} - -void FirstOrderModelIG::UfModelTreeGenerator::makeModel(TheoryModel* m, - uf::UfModelTree& tree) -{ - for (int j = 0; j < 2; j++) - { - for (int k = 0; k < 2; k++) - { - for (std::map<Node, Node>::iterator it = d_set_values[j][k].begin(); - it != d_set_values[j][k].end(); - ++it) - { - tree.setValue(m, it->first, it->second, k == 1); - } - } - } - if (!d_default_value.isNull()) - { - tree.setDefaultValue(m, d_default_value); - } - tree.simplify(); -} - -void FirstOrderModelIG::UfModelTreeGenerator::clear() -{ - d_default_value = Node::null(); - for (int j = 0; j < 2; j++) - { - for (int k = 0; k < 2; k++) - { - d_set_values[j][k].clear(); - } - } - d_defaults.clear(); -} - -FirstOrderModelIG::FirstOrderModelIG(QuantifiersEngine * qe, context::Context* c, std::string name) : -FirstOrderModel(qe, c,name) { - -} - -void FirstOrderModelIG::processInitialize( bool ispre ){ - if( ispre ){ - //rebuild models - d_uf_model_tree.clear(); - d_uf_model_gen.clear(); - } -} - -void FirstOrderModelIG::processInitializeModelForTerm( Node n ){ - if( n.getKind()==APPLY_UF ){ - Node op = n.getOperator(); - if( d_uf_model_tree.find( op )==d_uf_model_tree.end() ){ - TypeNode tn = op.getType(); - tn = tn[ (int)tn.getNumChildren()-1 ]; - //only generate models for predicates and functions with uninterpreted range types - //if( tn==NodeManager::currentNM()->booleanType() || tn.isSort() ){ - d_uf_model_tree[ op ] = uf::UfModelTree( op ); - d_uf_model_gen[ op ].clear(); - //} - } - } - /* - if( n.getType().isArray() ){ - while( n.getKind()==STORE ){ - n = n[0]; - } - Node nn = getRepresentative( n ); - if( d_array_model.find( nn )==d_array_model.end() ){ - d_array_model[nn] = arrays::ArrayModel( nn, this ); - } - } - */ -} - -//for evaluation of quantifier bodies - -void FirstOrderModelIG::resetEvaluate(){ - d_eval_uf_use_default.clear(); - d_eval_uf_model.clear(); - d_eval_term_index_order.clear(); -} - -//if evaluate( n ) = eVal, -// let n' = ri * n be the formula n instantiated with the current values in r_iter -// if eVal = 1, then n' is true, if eVal = -1, then n' is false, -// if eVal = 0, then n' cannot be proven to be equal to phaseReq -// if eVal is not 0, then -// each n{ri->d_index[0]/x_0...ri->d_index[depIndex]/x_depIndex, */x_(depIndex+1) ... */x_n } is equivalent in the current model -int FirstOrderModelIG::evaluate( Node n, int& depIndex, RepSetIterator* ri ){ - Debug("fmf-eval-debug2") << "Evaluate " << n << std::endl; - //Notice() << "Eval " << n << std::endl; - if( n.getKind()==NOT ){ - int val = evaluate( n[0], depIndex, ri ); - return val==1 ? -1 : ( val==-1 ? 1 : 0 ); - }else if( n.getKind()==OR || n.getKind()==AND ){ - int baseVal = n.getKind()==AND ? 1 : -1; - int eVal = baseVal; - int posDepIndex = ri->getNumTerms(); - int negDepIndex = -1; - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - //evaluate subterm - int childDepIndex; - Node nn = n[i]; - int eValT = evaluate( nn, childDepIndex, ri ); - if( eValT==baseVal ){ - if( eVal==baseVal ){ - if( childDepIndex>negDepIndex ){ - negDepIndex = childDepIndex; - } - } - }else if( eValT==-baseVal ){ - eVal = -baseVal; - if( childDepIndex<posDepIndex ){ - posDepIndex = childDepIndex; - if( posDepIndex==-1 ){ - break; - } - } - }else if( eValT==0 ){ - if( eVal==baseVal ){ - eVal = 0; - } - } - } - if( eVal!=0 ){ - depIndex = eVal==-baseVal ? posDepIndex : negDepIndex; - return eVal; - }else{ - return 0; - } - }else if( n.getKind()==EQUAL && n[0].getType().isBoolean() ){ - int depIndex1; - int eVal = evaluate( n[0], depIndex1, ri ); - if( eVal!=0 ){ - int depIndex2; - int eVal2 = evaluate( n[1], depIndex2, ri ); - if( eVal2!=0 ){ - depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2; - return eVal==eVal2 ? 1 : -1; - } - } - return 0; - }else if( n.getKind()==ITE ){ - int depIndex1, depIndex2; - int eVal = evaluate( n[0], depIndex1, ri ); - if( eVal==0 ){ - //evaluate children to see if they are the same value - int eval1 = evaluate( n[1], depIndex1, ri ); - if( eval1!=0 ){ - int eval2 = evaluate( n[1], depIndex2, ri ); - if( eval1==eval2 ){ - depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2; - return eval1; - } - } - }else{ - int eValT = evaluate( n[eVal==1 ? 1 : 2], depIndex2, ri ); - depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2; - return eValT; - } - return 0; - }else if( n.getKind()==FORALL ){ - return 0; - }else{ - //Debug("fmf-eval-debug") << "Evaluate literal " << n << std::endl; - int retVal = 0; - depIndex = ri->getNumTerms()-1; - Node val = evaluateTerm( n, depIndex, ri ); - if( !val.isNull() ){ - if( areEqual( val, d_true ) ){ - retVal = 1; - }else if( areEqual( val, d_false ) ){ - retVal = -1; - }else{ - if( val.getKind()==EQUAL ){ - if( areEqual( val[0], val[1] ) ){ - retVal = 1; - }else if( areDisequal( val[0], val[1] ) ){ - retVal = -1; - } - } - } - } - if( retVal!=0 ){ - Debug("fmf-eval-debug") << "Evaluate literal: return " << retVal << ", depIndex = " << depIndex << std::endl; - }else{ - Trace("fmf-eval-amb") << "Neither true nor false : " << n << std::endl; - Trace("fmf-eval-amb") << " value : " << val << std::endl; - } - return retVal; - } -} - -Node FirstOrderModelIG::evaluateTerm( Node n, int& depIndex, RepSetIterator* ri ){ - //Message() << "Eval term " << n << std::endl; - Node val; - depIndex = ri->getNumTerms()-1; - //check the type of n - if( n.getKind()==INST_CONSTANT ){ - int v = n.getAttribute(InstVarNumAttribute()); - depIndex = ri->getIndexOrder( v ); - val = ri->getCurrentTerm( v ); - }else if( n.getKind()==ITE ){ - int depIndex1, depIndex2; - int eval = evaluate( n[0], depIndex1, ri ); - if( eval==0 ){ - //evaluate children to see if they are the same - Node val1 = evaluateTerm( n[ 1 ], depIndex1, ri ); - Node val2 = evaluateTerm( n[ 2 ], depIndex2, ri ); - if( val1==val2 ){ - val = val1; - depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2; - }else{ - return Node::null(); - } - }else{ - val = evaluateTerm( n[ eval==1 ? 1 : 2 ], depIndex2, ri ); - depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2; - } - }else{ - std::vector< int > children_depIndex; - //default term evaluate : evaluate all children, recreate the value - val = evaluateTermDefault( n, depIndex, children_depIndex, ri ); - Trace("fmf-eval-debug") << "Evaluate term, value from " << n << " is " << val << std::endl; - if( !val.isNull() ){ - bool setVal = false; - //custom ways of evaluating terms - if( n.getKind()==APPLY_UF ){ - Node op = n.getOperator(); - //Debug("fmf-eval-debug") << "Evaluate term " << n << " (" << gn << ")" << std::endl; - //if it is a defined UF, then consult the interpretation - if( d_uf_model_tree.find( op )!=d_uf_model_tree.end() ){ - int argDepIndex = 0; - //make the term model specifically for n - makeEvalUfModel( n ); - //now, consult the model - if( d_eval_uf_use_default[n] ){ - Trace("fmf-eval-debug") << "get default" << std::endl; - val = d_uf_model_tree[ op ].getValue( this, val, argDepIndex ); - }else{ - Trace("fmf-eval-debug") << "get uf model" << std::endl; - val = d_eval_uf_model[ n ].getValue( this, val, argDepIndex ); - } - //Debug("fmf-eval-debug") << "Evaluate term " << n << " (" << gn << ")" << std::endl; - //d_eval_uf_model[ n ].debugPrint("fmf-eval-debug", d_qe ); - Assert( !val.isNull() ); - //recalculate the depIndex - depIndex = -1; - for( int i=0; i<argDepIndex; i++ ){ - int index = d_eval_uf_use_default[n] ? i : d_eval_term_index_order[n][i]; - Debug("fmf-eval-debug") << "Add variables from " << index << "..." << std::endl; - if( children_depIndex[index]>depIndex ){ - depIndex = children_depIndex[index]; - } - } - setVal = true; - }else{ - Trace("fmf-eval-debug") << "No model." << std::endl; - } - } - //if not set already, rewrite and consult model for interpretation - if( !setVal ){ - val = Rewriter::rewrite( val ); - if( !val.isConst() ){ - return Node::null(); - } - } - Trace("fmf-eval-debug") << "Evaluate term " << n << " = "; - Trace("fmf-eval-debug") << getRepresentative(val); - Trace("fmf-eval-debug") << " (term " << val << "), depIndex = " << depIndex << std::endl; - } - } - return val; -} - -Node FirstOrderModelIG::evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex, RepSetIterator* ri ){ - depIndex = -1; - if( n.getNumChildren()==0 ){ - return n; - }else{ - bool isInterp = n.getKind()!=APPLY_UF; - //first we must evaluate the arguments - std::vector< Node > children; - if( n.getMetaKind()==kind::metakind::PARAMETERIZED ){ - children.push_back( n.getOperator() ); - } - //for each argument, calculate its value, and the variables its value depends upon - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - childDepIndex.push_back( -1 ); - Node nn = evaluateTerm( n[i], childDepIndex[i], ri ); - if( nn.isNull() ){ - depIndex = ri->getNumTerms()-1; - return nn; - }else{ - if( childDepIndex[i]>depIndex ){ - depIndex = childDepIndex[i]; - } - if( isInterp ){ - if( !nn.isConst() ) { - nn = getRepresentative( nn ); - } - } - children.push_back( nn ); - } - } - //recreate the value - Node val = NodeManager::currentNM()->mkNode( n.getKind(), children ); - return val; - } -} - -void FirstOrderModelIG::makeEvalUfModel( Node n ){ - if( d_eval_uf_model.find( n )==d_eval_uf_model.end() ){ - makeEvalUfIndexOrder( n ); - if( !d_eval_uf_use_default[n] ){ - Node op = n.getOperator(); - d_eval_uf_model[n] = uf::UfModelTree( op, d_eval_term_index_order[n] ); - d_uf_model_gen[op].makeModel( this, d_eval_uf_model[n] ); - //Debug("fmf-index-order") << "Make model for " << n << " : " << std::endl; - //d_eval_uf_model[n].debugPrint( std::cout, d_qe->getModel(), 2 ); - } - } -} - -struct sortGetMaxVariableNum { - std::map< Node, int > d_max_var_num; - int computeMaxVariableNum( Node n ){ - if( n.getKind()==INST_CONSTANT ){ - return n.getAttribute(InstVarNumAttribute()); - }else if( TermUtil::hasInstConstAttr(n) ){ - int maxVal = -1; - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - int val = getMaxVariableNum( n[i] ); - if( val>maxVal ){ - maxVal = val; - } - } - return maxVal; - }else{ - return -1; - } - } - int getMaxVariableNum( Node n ){ - std::map< Node, int >::iterator it = d_max_var_num.find( n ); - if( it==d_max_var_num.end() ){ - int num = computeMaxVariableNum( n ); - d_max_var_num[n] = num; - return num; - }else{ - return it->second; - } - } - bool operator() (Node i,Node j) { return (getMaxVariableNum(i)<getMaxVariableNum(j));} -}; - -void FirstOrderModelIG::makeEvalUfIndexOrder( Node n ){ - if( d_eval_term_index_order.find( n )==d_eval_term_index_order.end() ){ - //sort arguments in order of least significant vs. most significant variable in default ordering - std::map< Node, std::vector< int > > argIndex; - std::vector< Node > args; - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( argIndex.find( n[i] )==argIndex.end() ){ - args.push_back( n[i] ); - } - argIndex[n[i]].push_back( i ); - } - sortGetMaxVariableNum sgmvn; - std::sort( args.begin(), args.end(), sgmvn ); - for( int i=0; i<(int)args.size(); i++ ){ - for( int j=0; j<(int)argIndex[ args[i] ].size(); j++ ){ - d_eval_term_index_order[n].push_back( argIndex[ args[i] ][j] ); - } - } - bool useDefault = true; - for( int i=0; i<(int)d_eval_term_index_order[n].size(); i++ ){ - if( i!=d_eval_term_index_order[n][i] ){ - useDefault = false; - break; - } - } - d_eval_uf_use_default[n] = useDefault; - Debug("fmf-index-order") << "Will consider the following index ordering for " << n << " : "; - for( int i=0; i<(int)d_eval_term_index_order[n].size(); i++ ){ - Debug("fmf-index-order") << d_eval_term_index_order[n][i] << " "; - } - Debug("fmf-index-order") << std::endl; - } -} - FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name) : FirstOrderModel(qe, c, name){ @@ -989,128 +521,6 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) { return NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, curr); } -FirstOrderModelAbs::FirstOrderModelAbs(QuantifiersEngine * qe, context::Context* c, std::string name) : -FirstOrderModel(qe, c, name) { - -} - -FirstOrderModelAbs::~FirstOrderModelAbs() -{ - for(std::map<Node, AbsDef*>::iterator i = d_models.begin(); i != d_models.end(); ++i) { - delete (*i).second; - } -} - -void FirstOrderModelAbs::processInitialize( bool ispre ) { - if( !ispre ){ - Trace("ambqi-debug") << "Process initialize" << std::endl; - for( std::map<Node, AbsDef * >::iterator it = d_models.begin(); it != d_models.end(); ++it ) { - Node op = it->first; - TypeNode tno = op.getType(); - Trace("ambqi-debug") << " Init " << op << " " << tno << std::endl; - for( unsigned i=0; i<tno.getNumChildren(); i++) { - //make sure a representative of the type exists - if( !d_rep_set.hasType( tno[i] ) ){ - Node e = getSomeDomainElement( tno[i] ); - Trace("ambqi-debug") << " * Initialize type " << tno[i] << ", add "; - Trace("ambqi-debug") << e << " " << e.getType() << std::endl; - //d_rep_set.add( e ); - } - } - } - } -} - -unsigned FirstOrderModelAbs::getRepresentativeId( TNode n ) { - TNode r = getUsedRepresentative( n ); - std::map< TNode, unsigned >::iterator it = d_rep_id.find( r ); - if( it!=d_rep_id.end() ){ - return it->second; - }else{ - return 0; - } -} - -TNode FirstOrderModelAbs::getUsedRepresentative( TNode n ) { - if( hasTerm( n ) ){ - if( n.getType().isBoolean() ){ - return areEqual(n, d_true) ? d_true : d_false; - }else{ - return getRepresentative( n ); - } - }else{ - Trace("qint-debug") << "Get rep " << n << " " << n.getType() << std::endl; - Assert( d_rep_set.hasType( n.getType() ) && !d_rep_set.d_type_reps[n.getType()].empty() ); - return d_rep_set.d_type_reps[n.getType()][0]; - } -} - -Node FirstOrderModelAbs::getFunctionValue(Node op, const char* argPrefix ) { - if( d_models_valid[op] ){ - Trace("ambqi-debug") << "Get function value for " << op << std::endl; - TypeNode type = op.getType(); - std::vector< Node > vars; - for( size_t i=0; i<type.getNumChildren()-1; i++ ){ - std::stringstream ss; - ss << argPrefix << (i+1); - Node b = NodeManager::currentNM()->mkBoundVar( ss.str(), type[i] ); - vars.push_back( b ); - } - Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, vars); - Node curr = d_models[op]->getFunctionValue( this, op, vars ); - Node fv = NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, curr); - Trace("ambqi-debug") << "Return " << fv << std::endl; - return fv; - }else{ - - } - return Node::null(); -} - -void FirstOrderModelAbs::processInitializeModelForTerm( Node n ) { - if( n.getKind()==APPLY_UF || n.getKind()==VARIABLE || n.getKind()==SKOLEM ){ - Node op = n.getKind()==APPLY_UF ? n.getOperator() : n; - if( d_models.find(op)==d_models.end()) { - Trace("abmqi-debug") << "init model for " << op << std::endl; - d_models[op] = new AbsDef; - d_models_valid[op] = false; - } - } -} - -void FirstOrderModelAbs::collectEqVars( TNode q, TNode n, std::map< int, bool >& eq_vars ) { - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - if( n.getKind()==EQUAL && n[i].getKind()==BOUND_VARIABLE ){ - int v = getVariableId( q, n[i] ); - Assert( v>=0 && v<(int)q[0].getNumChildren() ); - eq_vars[v] = true; - } - collectEqVars( q, n[i], eq_vars ); - } -} - -void FirstOrderModelAbs::processInitializeQuantifier( Node q ) { - if( d_var_order.find( q )==d_var_order.end() ){ - std::map< int, bool > eq_vars; - for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ - eq_vars[i] = false; - } - collectEqVars( q, q[1], eq_vars ); - for( unsigned r=0; r<2; r++ ){ - for( std::map< int, bool >::iterator it = eq_vars.begin(); it != eq_vars.end(); ++it ){ - if( it->second==(r==1) ){ - d_var_index[q][it->first] = d_var_order[q].size(); - d_var_order[q].push_back( it->first ); - } - } - } - } -} - -Node FirstOrderModelAbs::getVariable( Node q, unsigned i ) { - return q[0][d_var_order[q][i]]; -} - } /* CVC4::theory::quantifiers namespace */ } /* CVC4::theory namespace */ } /* CVC4 namespace */ diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index 7da5b2088..b96b42dc2 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -42,15 +42,10 @@ namespace quantifiers { class TermDb; -class FirstOrderModelIG; - namespace fmcheck { class FirstOrderModelFmc; }/* CVC4::theory::quantifiers::fmcheck namespace */ -class FirstOrderModelQInt; -class FirstOrderModelAbs; - struct IsStarAttributeId {}; typedef expr::Attribute<IsStarAttributeId, bool> IsStarAttribute; @@ -94,10 +89,7 @@ class FirstOrderModel : public TheoryModel public: FirstOrderModel(QuantifiersEngine* qe, context::Context* c, std::string name); - virtual FirstOrderModelIG* asFirstOrderModelIG() { return nullptr; } virtual fmcheck::FirstOrderModelFmc* asFirstOrderModelFmc() { return nullptr; } - virtual FirstOrderModelQInt* asFirstOrderModelQInt() { return nullptr; } - virtual FirstOrderModelAbs* asFirstOrderModelAbs() { return nullptr; } /** assert quantifier */ void assertQuantifier( Node n ); /** get number of asserted quantifiers */ @@ -172,11 +164,11 @@ class FirstOrderModel : public TheoryModel /** get variable id */ std::map<Node, std::map<Node, int> > d_quant_var_id; /** process initialize model for term */ - virtual void processInitializeModelForTerm(Node n) = 0; + virtual void processInitializeModelForTerm(Node n) {} /** process initialize quantifier */ virtual void processInitializeQuantifier(Node q) {} /** process initialize */ - virtual void processInitialize(bool ispre) = 0; + virtual void processInitialize(bool ispre) {} private: // list of inactive quantified formulas @@ -193,85 +185,6 @@ class FirstOrderModel : public TheoryModel void computeModelBasisArgAttribute(Node n); };/* class FirstOrderModel */ -class FirstOrderModelIG : public FirstOrderModel -{ - public: // for Theory UF: - /** class for generating models for uninterpreted functions - * - * This implements the model construction from page 6 of Reynolds et al, - * "Quantifier Instantiation Techniques for Finite Model Finding in SMT", - * CADE 2013. - */ - class UfModelTreeGenerator - { - public: - UfModelTreeGenerator() {} - ~UfModelTreeGenerator() {} - /** set default value */ - void setDefaultValue(Node v) { d_default_value = v; } - /** set value */ - void setValue( - TheoryModel* m, Node n, Node v, bool ground = true, bool isReq = true); - /** make model */ - void makeModel(TheoryModel* m, uf::UfModelTree& tree); - /** reset */ - void clear(); - - public: - /** the overall default value */ - Node d_default_value; - /** - * Stores (required, ground) values in key, value pairs of the form - * ( P( a, b ), c ), which indicates P( a, b ) has value c in the model. - * The "non-ground" values indicate that the key has a "model-basis" - * variable, for example, ( P( _, b ), c ) indicates that P( x, b ) has the - * value b for any value of x. - */ - std::map<Node, Node> d_set_values[2][2]; - /** stores the set of non-ground keys in the above maps */ - std::vector<Node> d_defaults; - /** - * Returns the term corresponding to the intersection of n1 and n2, if it - * exists, for example, for P( _, a ) and P( b, _ ), this method returns - * P( b, a ), where _ is the "model basis" variable. We take into account - * equality between arguments, so if a=b, then the intersection of P( a, a ) - * and P( b, _ ) is P( a, a ). - */ - Node getIntersection(TheoryModel* m, Node n1, Node n2, bool& isGround); - }; - /** models for each UF operator */ - std::map<Node, uf::UfModelTree> d_uf_model_tree; - /** model generators for each UF operator */ - std::map<Node, UfModelTreeGenerator> d_uf_model_gen; - - private: - //map from terms to the models used to calculate their value - std::map< Node, bool > d_eval_uf_use_default; - std::map< Node, uf::UfModelTree > d_eval_uf_model; - void makeEvalUfModel( Node n ); - //index ordering to use for each term - std::map< Node, std::vector< int > > d_eval_term_index_order; - void makeEvalUfIndexOrder( Node n ); -//the following functions are for evaluating quantifier bodies -public: - FirstOrderModelIG(QuantifiersEngine * qe, context::Context* c, std::string name); - - FirstOrderModelIG* asFirstOrderModelIG() override { return this; } - // initialize the model - void processInitialize(bool ispre) override; - //for initialize model - void processInitializeModelForTerm(Node n) override; - /** reset evaluation */ - void resetEvaluate(); - /** evaluate functions */ - int evaluate( Node n, int& depIndex, RepSetIterator* ri ); - Node evaluateTerm( Node n, int& depIndex, RepSetIterator* ri ); -private: - //default evaluate term function - Node evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex, RepSetIterator* ri ); -};/* class FirstOrderModelIG */ - - namespace fmcheck { class Def; @@ -301,36 +214,6 @@ class FirstOrderModelFmc : public FirstOrderModel }/* CVC4::theory::quantifiers::fmcheck namespace */ -class AbsDef; - -class FirstOrderModelAbs : public FirstOrderModel -{ - public: - std::map< Node, AbsDef * > d_models; - std::map< Node, bool > d_models_valid; - std::map< TNode, unsigned > d_rep_id; - std::map< TypeNode, unsigned > d_domain; - std::map< Node, std::vector< int > > d_var_order; - std::map< Node, std::map< int, int > > d_var_index; - - private: - /** get current model value */ - void processInitializeModelForTerm(Node n) override; - void processInitializeQuantifier(Node q) override; - void collectEqVars( TNode q, TNode n, std::map< int, bool >& eq_vars ); - TNode getUsedRepresentative( TNode n ); - - public: - FirstOrderModelAbs(QuantifiersEngine * qe, context::Context* c, std::string name); - ~FirstOrderModelAbs() override; - FirstOrderModelAbs* asFirstOrderModelAbs() override { return this; } - void processInitialize(bool ispre) override; - unsigned getRepresentativeId( TNode n ); - bool isValidType( TypeNode tn ) { return d_domain.find( tn )!=d_domain.end(); } - Node getFunctionValue(Node op, const char* argPrefix ); - Node getVariable( Node q, unsigned i ); -}; - }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/fmf/ambqi_builder.cpp b/src/theory/quantifiers/fmf/ambqi_builder.cpp deleted file mode 100644 index f2b131f21..000000000 --- a/src/theory/quantifiers/fmf/ambqi_builder.cpp +++ /dev/null @@ -1,971 +0,0 @@ -/********************* */ -/*! \file ambqi_builder.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Implementation of abstract MBQI builder - **/ - -#include "theory/quantifiers/fmf/ambqi_builder.h" - -#include "base/cvc4_check.h" -#include "options/quantifiers_options.h" -#include "theory/quantifiers/instantiate.h" -#include "theory/quantifiers/term_database.h" -#include "theory/quantifiers/term_util.h" - -using namespace std; -using namespace CVC4::kind; -using namespace CVC4::context; - -namespace CVC4 { -namespace theory { -namespace quantifiers { - - -void AbsDef::construct_func( FirstOrderModelAbs * m, std::vector< TNode >& fapps, unsigned depth ) { - d_def.clear(); - Assert( !fapps.empty() ); - if( depth==fapps[0].getNumChildren() ){ - //if( fapps.size()>1 ){ - // for( unsigned i=0; i<fapps.size(); i++ ){ - // std::cout << "...." << fapps[i] << " -> " << m->getRepresentativeId( fapps[i] ) << std::endl; - // } - //} - //get representative in model for this term - d_value = m->getRepresentativeId( fapps[0] ); - Assert( d_value!=val_none ); - }else{ - TypeNode tn = fapps[0][depth].getType(); - std::map< unsigned, std::vector< TNode > > fapp_child; - - //partition based on evaluations of fapps[1][depth]....fapps[n][depth] - for( unsigned i=0; i<fapps.size(); i++ ){ - unsigned r = m->getRepresentativeId( fapps[i][depth] ); - Assert( r < 32 ); - fapp_child[r].push_back( fapps[i] ); - } - - //do completion - std::map< unsigned, unsigned > fapp_child_index; - unsigned def = m->d_domain[ tn ]; - unsigned minSize = fapp_child.begin()->second.size(); - unsigned minSizeIndex = fapp_child.begin()->first; - for( std::map< unsigned, std::vector< TNode > >::iterator it = fapp_child.begin(); it != fapp_child.end(); ++it ){ - fapp_child_index[it->first] = ( 1 << it->first ); - def = def & ~( 1 << it->first ); - if( it->second.size()<minSize ){ - minSize = it->second.size(); - minSizeIndex = it->first; - } - } - fapp_child_index[minSizeIndex] |= def; - d_default = fapp_child_index[minSizeIndex]; - - //construct children - for( std::map< unsigned, std::vector< TNode > >::iterator it = fapp_child.begin(); it != fapp_child.end(); ++it ){ - Trace("abs-model-debug") << "Construct " << it->first << " : " << fapp_child_index[it->first] << " : "; - const RepSet* rs = m->getRepSet(); - debugPrintUInt("abs-model-debug", - rs->getNumRepresentatives(tn), - fapp_child_index[it->first]); - Trace("abs-model-debug") << " : " << it->second.size() << " terms." << std::endl; - d_def[fapp_child_index[it->first]].construct_func( m, it->second, depth+1 ); - } - } -} - -void AbsDef::simplify( FirstOrderModelAbs * m, TNode q, TNode n, unsigned depth ) { - if( d_value==val_none && !d_def.empty() ){ - //process the default - std::map< unsigned, AbsDef >::iterator defd = d_def.find( d_default ); - Assert( defd!=d_def.end() ); - unsigned newDef = d_default; - std::vector< unsigned > to_erase; - defd->second.simplify( m, q, n, depth+1 ); - int defVal = defd->second.d_value; - bool isConstant = ( defVal!=val_none ); - //process each child - for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){ - if( it->first!=d_default ){ - it->second.simplify( m, q, n, depth+1 ); - if( it->second.d_value==defVal && it->second.d_value!=val_none ){ - newDef = newDef | it->first; - to_erase.push_back( it->first ); - }else{ - isConstant = false; - } - } - } - if( !to_erase.empty() ){ - //erase old default - int defVal = defd->second.d_value; - d_def.erase( d_default ); - //set new default - d_default = newDef; - d_def[d_default].construct_def_entry( m, q, n, defVal, depth+1 ); - //erase redundant entries - for( unsigned i=0; i<to_erase.size(); i++ ){ - d_def.erase( to_erase[i] ); - } - } - //if constant, propagate the value upwards - if( isConstant ){ - d_value = defVal; - }else{ - d_value = val_none; - } - } -} - -void AbsDef::debugPrintUInt( const char * c, unsigned dSize, unsigned u ) const{ - for( unsigned i=0; i<dSize; i++ ){ - Trace(c) << ( ( u & ( 1 << i ) )!=0 ? "1" : "0"); - } - //Trace(c) << "("; - //for( unsigned i=0; i<32; i++ ){ - // Trace(c) << ( ( u & ( 1 << i ) )!=0 ? "1" : "0"); - //} - //Trace(c) << ")"; -} - -void AbsDef::debugPrint( const char * c, FirstOrderModelAbs * m, TNode f, unsigned depth ) const{ - if( Trace.isOn(c) ){ - if( depth==f.getNumChildren() ){ - for( unsigned i=0; i<depth; i++ ){ Trace(c) << " ";} - Trace(c) << "V[" << d_value << "]" << std::endl; - }else{ - TypeNode tn = f[depth].getType(); - const RepSet* rs = m->getRepSet(); - unsigned dSize = rs->getNumRepresentatives(tn); - Assert( dSize<32 ); - for( std::map< unsigned, AbsDef >::const_iterator it = d_def.begin(); it != d_def.end(); ++it ){ - for( unsigned i=0; i<depth; i++ ){ Trace(c) << " ";} - debugPrintUInt( c, dSize, it->first ); - if( it->first==d_default ){ - Trace(c) << "*"; - } - if( it->second.d_value!=val_none ){ - Trace(c) << " -> V[" << it->second.d_value << "]"; - } - Trace(c) << std::endl; - it->second.debugPrint( c, m, f, depth+1 ); - } - } - } -} - -bool AbsDef::addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe, TNode q, std::vector< Node >& terms, int& inst, unsigned depth ) { - if( inst==0 || !options::fmfOneInstPerRound() ){ - if( d_value==1 ){ - //instantiations are all true : ignore this - return true; - }else{ - if( depth==q[0].getNumChildren() ){ - if (qe->getInstantiate()->addInstantiation(q, terms, true)) - { - Trace("ambqi-inst-debug") << "-> Added instantiation." << std::endl; - inst++; - return true; - }else{ - Trace("ambqi-inst-debug") << "-> Failed to add instantiation." << std::endl; - //we are incomplete - return false; - } - }else{ - bool osuccess = true; - TypeNode tn = m->getVariable( q, depth ).getType(); - for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){ - //get witness term - unsigned index = 0; - bool success; - do { - success = false; - index = getId( it->first, index ); - if( index<32 ){ - const RepSet* rs = m->getRepSet(); - Assert(index < rs->getNumRepresentatives(tn)); - terms[m->d_var_order[q][depth]] = - rs->getRepresentative(tn, index); - if( !it->second.addInstantiations( m, qe, q, terms, inst, depth+1 ) && inst==0 ){ - //if we are incomplete, and have not yet added an instantiation, keep trying - index++; - Trace("ambqi-inst-debug") << "At depth " << depth << ", failed branch, no instantiations and incomplete, increment index : " << index << std::endl; - }else{ - success = true; - } - } - }while( !qe->inConflict() && !success && index<32 ); - //mark if we are incomplete - osuccess = osuccess && success; - } - return osuccess; - } - } - }else{ - return true; - } -} - -void AbsDef::construct_entry( std::vector< unsigned >& entry, std::vector< bool >& entry_def, int v, unsigned depth ) { - if( depth==entry.size() ){ - d_value = v; - }else{ - d_def[entry[depth]].construct_entry( entry, entry_def, v, depth+1 ); - if( entry_def[depth] ){ - d_default = entry[depth]; - } - } -} - -void AbsDef::get_defs( unsigned u, std::vector< AbsDef * >& defs ) { - for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){ - if( ( u & it->first )!=0 ){ - Assert( (u & it->first)==u ); - defs.push_back( &it->second ); - } - } -} - -void AbsDef::construct_normalize( FirstOrderModelAbs * m, TNode q, std::vector< AbsDef * >& defs, unsigned depth ) { - if( depth==q[0].getNumChildren() ){ - Assert( defs.size()==1 ); - d_value = defs[0]->d_value; - }else{ - TypeNode tn = m->getVariable( q, depth ).getType(); - unsigned def = m->d_domain[tn]; - for( unsigned i=0; i<defs.size(); i++ ){ - //process each simple child - for( std::map< unsigned, AbsDef >::iterator itd = defs[i]->d_def.begin(); itd != defs[i]->d_def.end(); ++itd ){ - if( isSimple( itd->first ) && ( def & itd->first )!=0 ){ - def &= ~( itd->first ); - //process this value - std::vector< AbsDef * > cdefs; - for( unsigned j=0; j<defs.size(); j++ ){ - defs[j]->get_defs( itd->first, cdefs ); - } - d_def[itd->first].construct_normalize( m, q, cdefs, depth+1 ); - if( def==0 ){ - d_default = itd->first; - break; - } - } - } - if( def==0 ){ - break; - } - } - if( def!=0 ){ - d_default = def; - //process the default - std::vector< AbsDef * > cdefs; - for( unsigned j=0; j<defs.size(); j++ ){ - defs[j]->get_defs( d_default, cdefs ); - } - d_def[d_default].construct_normalize( m, q, cdefs, depth+1 ); - } - } -} - -void AbsDef::construct_def_entry( FirstOrderModelAbs * m, TNode q, TNode n, int v, unsigned depth ) { - d_value = v; - if( depth<n.getNumChildren() ){ - TypeNode tn = q.isNull() ? n[depth].getType() : m->getVariable( q, depth ).getType(); - unsigned dom = m->d_domain[tn] ; - d_def[dom].construct_def_entry( m, q, n, v, depth+1 ); - d_default = dom; - } -} - -void AbsDef::apply_ucompose( FirstOrderModelAbs * m, TNode q, - std::vector< unsigned >& entry, std::vector< bool >& entry_def, - std::vector< int >& terms, std::map< unsigned, int >& vchildren, - AbsDef * a, unsigned depth ) { - if( depth==terms.size() ){ - if( Trace.isOn("ambqi-check-debug2") ){ - Trace("ambqi-check-debug2") << "Add entry ( "; - const RepSet* rs = m->getRepSet(); - for( unsigned i=0; i<entry.size(); i++ ){ - unsigned dSize = - rs->getNumRepresentatives(m->getVariable(q, i).getType()); - debugPrintUInt( "ambqi-check-debug2", dSize, entry[i] ); - Trace("ambqi-check-debug2") << " "; - } - Trace("ambqi-check-debug2") << ")" << std::endl; - } - a->construct_entry( entry, entry_def, d_value ); - }else{ - unsigned id; - if( terms[depth]==val_none ){ - //a variable - std::map< unsigned, int >::iterator itv = vchildren.find( depth ); - Assert( itv!=vchildren.end() ); - unsigned prev_v = entry[itv->second]; - bool prev_vd = entry_def[itv->second]; - for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){ - entry[itv->second] = it->first & prev_v; - entry_def[itv->second] = ( it->first==d_default ) && prev_vd; - if( entry[itv->second]!=0 ){ - it->second.apply_ucompose( m, q, entry, entry_def, terms, vchildren, a, depth+1 ); - } - } - entry[itv->second] = prev_v; - entry_def[itv->second] = prev_vd; - }else{ - id = (unsigned)terms[depth]; - Assert( id<32 ); - unsigned fid = 1 << id; - std::map< unsigned, AbsDef >::iterator it = d_def.find( fid ); - if( it!=d_def.end() ){ - it->second.apply_ucompose( m, q, entry, entry_def, terms, vchildren, a, depth+1 ); - }else{ - d_def[d_default].apply_ucompose( m, q, entry, entry_def, terms, vchildren, a, depth+1 ); - } - } - } -} - -void AbsDef::construct_var_eq( FirstOrderModelAbs * m, TNode q, unsigned v1, unsigned v2, int curr, int currv, unsigned depth ) { - if( depth==q[0].getNumChildren() ){ - Assert( currv!=val_none ); - d_value = currv; - }else{ - TypeNode tn = m->getVariable( q, depth ).getType(); - unsigned dom = m->d_domain[tn]; - int vindex = depth==v1 ? 0 : ( depth==v2 ? 1 : val_none ); - if( vindex==val_none ){ - d_def[dom].construct_var_eq( m, q, v1, v2, curr, currv, depth+1 ); - d_default = dom; - }else{ - Assert( currv==val_none ); - if( curr==val_none ){ - unsigned numReps = m->getRepSet()->getNumRepresentatives(tn); - Assert( numReps < 32 ); - for( unsigned i=0; i<numReps; i++ ){ - curr = 1 << i; - d_def[curr].construct_var_eq( m, q, v1, v2, curr, currv, depth+1 ); - } - d_default = curr; - }else{ - d_def[curr].construct_var_eq( m, q, v1, v2, curr, 1, depth+1 ); - dom = dom & ~curr; - d_def[dom].construct_var_eq( m, q, v1, v2, curr, 0, depth+1 ); - d_default = dom; - } - } - } -} - -void AbsDef::construct_var( FirstOrderModelAbs * m, TNode q, unsigned v, int currv, unsigned depth ) { - if( depth==q[0].getNumChildren() ){ - Assert( currv!=val_none ); - d_value = currv; - }else{ - TypeNode tn = m->getVariable( q, depth ).getType(); - if( v==depth ){ - const unsigned numReps = m->getRepSet()->getNumRepresentatives(tn); - CVC4_CHECK(numReps > 0 && numReps < 32); - for( unsigned i=0; i<numReps; i++ ){ - d_def[ 1 << i ].construct_var( m, q, v, i, depth+1 ); - } - d_default = 1 << (numReps - 1); - }else{ - unsigned dom = m->d_domain[tn]; - d_def[dom].construct_var( m, q, v, currv, depth+1 ); - d_default = dom; - } - } -} - -void AbsDef::construct_compose( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef * f, - std::map< unsigned, AbsDef * >& children, - std::map< unsigned, int >& bchildren, std::map< unsigned, int >& vchildren, - std::vector< unsigned >& entry, std::vector< bool >& entry_def ) { - const RepSet* rs = m->getRepSet(); - if( n.getKind()==OR || n.getKind()==AND ){ - // short circuiting - for( std::map< unsigned, AbsDef * >::iterator it = children.begin(); it != children.end(); ++it ){ - if( ( it->second->d_value==0 && n.getKind()==AND ) || - ( it->second->d_value==1 && n.getKind()==OR ) ){ - //std::cout << "Short circuit " << it->second->d_value << " " << entry.size() << "/" << q[0].getNumChildren() << std::endl; - unsigned count = q[0].getNumChildren() - entry.size(); - for( unsigned i=0; i<count; i++ ){ - entry.push_back( m->d_domain[m->getVariable( q, entry.size() ).getType()] ); - entry_def.push_back( true ); - } - construct_entry( entry, entry_def, it->second->d_value ); - for( unsigned i=0; i<count; i++ ){ - entry.pop_back(); - entry_def.pop_back(); - } - return; - } - } - } - if( entry.size()==q[0].getNumChildren() ){ - if( f ){ - if( Trace.isOn("ambqi-check-debug2") ){ - for( unsigned i=0; i<entry.size(); i++ ){ Trace("ambqi-check-debug2") << " "; } - Trace("ambqi-check-debug2") << "Evaluate uninterpreted function entry..." << std::endl; - } - //we are composing with an uninterpreted function - std::vector< int > values; - values.resize( n.getNumChildren(), val_none ); - for( std::map< unsigned, AbsDef * >::iterator it = children.begin(); it != children.end(); ++it ){ - values[it->first] = it->second->d_value; - } - for( std::map< unsigned, int >::iterator it = bchildren.begin(); it != bchildren.end(); ++it ){ - values[it->first] = it->second; - } - //look up value(s) - f->apply_ucompose( m, q, entry, entry_def, values, vchildren, this ); - }else{ - bool incomplete = false; - //we are composing with an interpreted function - std::vector< TNode > values; - values.resize( n.getNumChildren(), TNode::null() ); - for( std::map< unsigned, AbsDef * >::iterator it = children.begin(); it != children.end(); ++it ){ - Trace("ambqi-check-debug2") << "composite : " << it->first << " : " << it->second->d_value; - if( it->second->d_value>=0 ){ - if (it->second->d_value - >= (int)rs->getNumRepresentatives(n[it->first].getType())) - { - std::cout << it->second->d_value << " " << n[it->first] << " " - << n[it->first].getType() << " " - << rs->getNumRepresentatives(n[it->first].getType()) - << std::endl; - } - Assert(it->second->d_value - < (int)rs->getNumRepresentatives(n[it->first].getType())); - values[it->first] = rs->getRepresentative(n[it->first].getType(), - it->second->d_value); - }else{ - incomplete = true; - } - Trace("ambqi-check-debug2") << " ->> " << values[it->first] << std::endl; - } - for( std::map< unsigned, int >::iterator it = bchildren.begin(); it != bchildren.end(); ++it ){ - Trace("ambqi-check-debug2") << " basic : " << it->first << " : " << it->second; - if( it->second>=0 ){ - Assert(it->second - < (int)rs->getNumRepresentatives(n[it->first].getType())); - values[it->first] = - rs->getRepresentative(n[it->first].getType(), it->second); - }else{ - incomplete = true; - } - Trace("ambqi-check-debug2") << " ->> " << values[it->first] << std::endl; - } - Assert( vchildren.empty() ); - if( incomplete ){ - Trace("ambqi-check-debug2") << "Construct incomplete entry." << std::endl; - - //if a child is unknown, we must return unknown - construct_entry( entry, entry_def, val_unk ); - }else{ - if( Trace.isOn("ambqi-check-debug2") ){ - for( unsigned i=0; i<entry.size(); i++ ){ Trace("ambqi-check-debug2") << " "; } - Trace("ambqi-check-debug2") << "Evaluate interpreted function entry ( "; - for( unsigned i=0; i<values.size(); i++ ){ - Assert( !values[i].isNull() ); - Trace("ambqi-check-debug2") << values[i] << " "; - } - Trace("ambqi-check-debug2") << ")..." << std::endl; - } - //evaluate - Node vv = NodeManager::currentNM()->mkNode( n.getKind(), values ); - vv = Rewriter::rewrite( vv ); - int v = m->getRepresentativeId( vv ); - construct_entry( entry, entry_def, v ); - } - } - }else{ - //take product of arguments - TypeNode tn = m->getVariable( q, entry.size() ).getType(); - Assert( m->isValidType( tn ) ); - unsigned def = m->d_domain[tn]; - if( Trace.isOn("ambqi-check-debug2") ){ - for( unsigned i=0; i<entry.size(); i++ ){ Trace("ambqi-check-debug2") << " "; } - Trace("ambqi-check-debug2") << "Take product of arguments" << std::endl; - } - for( std::map< unsigned, AbsDef * >::iterator it = children.begin(); it != children.end(); ++it ){ - Assert( it->second!=NULL ); - //process each child - for( std::map< unsigned, AbsDef >::iterator itd = it->second->d_def.begin(); itd != it->second->d_def.end(); ++itd ){ - if( itd->first!=it->second->d_default && ( def & itd->first )!=0 ){ - def &= ~( itd->first ); - //process this value - std::map< unsigned, AbsDef * > cchildren; - for( std::map< unsigned, AbsDef * >::iterator it2 = children.begin(); it2 != children.end(); ++it2 ){ - Assert( it2->second!=NULL ); - std::map< unsigned, AbsDef >::iterator itdf = it2->second->d_def.find( itd->first ); - if( itdf!=it2->second->d_def.end() ){ - cchildren[it2->first] = &itdf->second; - }else{ - Assert( it2->second->getDefault()!=NULL ); - cchildren[it2->first] = it2->second->getDefault(); - } - } - if( Trace.isOn("ambqi-check-debug2") ){ - for( unsigned i=0; i<entry.size(); i++ ){ Trace("ambqi-check-debug2") << " "; } - Trace("ambqi-check-debug2") << "...process : "; - debugPrintUInt("ambqi-check-debug2", - rs->getNumRepresentatives(tn), - itd->first); - Trace("ambqi-check-debug2") << " " << children.size() << " " << cchildren.size() << std::endl; - } - entry.push_back( itd->first ); - entry_def.push_back( def==0 ); - construct_compose( m, q, n, f, cchildren, bchildren, vchildren, entry, entry_def ); - entry_def.pop_back(); - entry.pop_back(); - if( def==0 ){ - break; - } - } - } - if( def==0 ){ - break; - } - } - if( def!=0 ){ - if( Trace.isOn("ambqi-check-debug2") ){ - for( unsigned i=0; i<entry.size(); i++ ){ Trace("ambqi-check-debug2") << " "; } - Trace("ambqi-check-debug2") << "Make default argument" << std::endl; - } - std::map< unsigned, AbsDef * > cdchildren; - for( std::map< unsigned, AbsDef * >::iterator it = children.begin(); it != children.end(); ++it ){ - Assert( it->second->getDefault()!=NULL ); - cdchildren[it->first] = it->second->getDefault(); - } - if( Trace.isOn("ambqi-check-debug2") ){ - for( unsigned i=0; i<entry.size(); i++ ){ Trace("ambqi-check-debug2") << " "; } - Trace("ambqi-check-debug2") << "...process default : "; - debugPrintUInt( - "ambqi-check-debug2", rs->getNumRepresentatives(tn), def); - Trace("ambqi-check-debug2") << " " << children.size() << " " << cdchildren.size() << std::endl; - } - entry.push_back( def ); - entry_def.push_back( true ); - construct_compose( m, q, n, f, cdchildren, bchildren, vchildren, entry, entry_def ); - entry_def.pop_back(); - entry.pop_back(); - } - } -} - -bool AbsDef::construct( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef * f, - std::map< unsigned, AbsDef * >& children, - std::map< unsigned, int >& bchildren, std::map< unsigned, int >& vchildren, - int varChCount ) { - if( Trace.isOn("ambqi-check-debug3") ){ - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - Trace("ambqi-check-debug3") << i << " : "; - Trace("ambqi-check-debug3") << ((children.find( i )!=children.end()) ? "X" : "."); - if( bchildren.find( i )!=bchildren.end() ){ - Trace("ambqi-check-debug3") << bchildren[i]; - }else{ - Trace("ambqi-check-debug3") << "."; - } - if( vchildren.find( i )!=vchildren.end() ){ - Trace("ambqi-check-debug3") << vchildren[i]; - }else{ - Trace("ambqi-check-debug3") << "."; - } - Trace("ambqi-check-debug3") << std::endl; - } - Trace("ambqi-check-debug3") << "varChCount : " << varChCount << std::endl; - } - if( varChCount==0 || f ){ - //short-circuit - if( n.getKind()==AND || n.getKind()==OR ){ - for( std::map< unsigned, int >::iterator it = bchildren.begin(); it !=bchildren.end(); ++it ){ - if( ( it->second==0 && n.getKind()==AND ) || - ( it->second==1 && n.getKind()==OR ) ){ - construct_def_entry( m, q, q[0], it->second ); - return true; - } - } - } - Trace("ambqi-check-debug2") << "Construct compose..." << std::endl; - std::vector< unsigned > entry; - std::vector< bool > entry_def; - if( f && varChCount>0 ){ - AbsDef unorm; - unorm.construct_compose( m, q, n, f, children, bchildren, vchildren, entry, entry_def ); - //normalize - std::vector< AbsDef* > defs; - defs.push_back( &unorm ); - construct_normalize( m, q, defs ); - }else{ - construct_compose( m, q, n, f, children, bchildren, vchildren, entry, entry_def ); - } - Assert( is_normalized() ); - return true; - }else if( varChCount==1 && ( n.getKind()==EQUAL && !n[0].getType().isBoolean() ) ){ - Trace("ambqi-check-debug2") << "Expand variable child..." << std::endl; - //expand the variable based on its finite domain - AbsDef a; - a.construct_var( m, q, vchildren.begin()->second, val_none ); - children[vchildren.begin()->first] = &a; - vchildren.clear(); - std::vector< unsigned > entry; - std::vector< bool > entry_def; - Trace("ambqi-check-debug2") << "Construct compose with variable..." << std::endl; - construct_compose( m, q, n, f, children, bchildren, vchildren, entry, entry_def ); - return true; - }else if( varChCount==2 && ( n.getKind()==EQUAL && !n[0].getType().isBoolean() ) ){ - Trace("ambqi-check-debug2") << "Construct variable equality..." << std::endl; - //efficient expansion of the equality - construct_var_eq( m, q, vchildren[0], vchildren[1], val_none, val_none ); - return true; - }else{ - return false; - } -} - -void AbsDef::negate() { - for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){ - it->second.negate(); - } - if( d_value==0 ){ - d_value = 1; - }else if( d_value==1 ){ - d_value = 0; - } -} - -Node AbsDef::getFunctionValue( FirstOrderModelAbs * m, TNode op, std::vector< Node >& vars, unsigned depth ) { - const RepSet* rs = m->getRepSet(); - if( depth==vars.size() ){ - TypeNode tn = op.getType(); - if( tn.getNumChildren()>0 ){ - tn = tn[tn.getNumChildren() - 1]; - } - if( d_value>=0 ){ - Assert(d_value < (int)rs->getNumRepresentatives(tn)); - if( tn.isBoolean() ){ - return NodeManager::currentNM()->mkConst( d_value==1 ); - }else{ - return rs->getRepresentative(tn, d_value); - } - }else{ - return Node::null(); - } - }else{ - TypeNode tn = vars[depth].getType(); - Node curr; - curr = d_def[d_default].getFunctionValue( m, op, vars, depth+1 ); - for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){ - if( it->first!=d_default ){ - unsigned id = getId( it->first ); - Assert(id < rs->getNumRepresentatives(tn)); - TNode n = rs->getRepresentative(tn, id); - Node fv = it->second.getFunctionValue( m, op, vars, depth+1 ); - if( !curr.isNull() && !fv.isNull() ){ - curr = NodeManager::currentNM()->mkNode( ITE, vars[depth].eqNode( n ), fv, curr ); - }else{ - curr = Node::null(); - } - } - } - return curr; - } -} - -bool AbsDef::isSimple( unsigned n ) { - return (n & (n - 1))==0; -} - -unsigned AbsDef::getId( unsigned n, unsigned start, unsigned end ) { - Assert( n!=0 ); - while( (n & ( 1 << start )) == 0 ){ - start++; - if( start==end ){ - return start; - } - } - return start; -} - -Node AbsDef::evaluate( FirstOrderModelAbs * m, TypeNode retTyp, std::vector< Node >& args ) { - std::vector< unsigned > iargs; - for( unsigned i=0; i<args.size(); i++ ){ - unsigned v = 1 << m->getRepresentativeId( args[i] ); - iargs.push_back( v ); - } - return evaluate( m, retTyp, iargs, 0 ); -} - -Node AbsDef::evaluate( FirstOrderModelAbs * m, TypeNode retTyp, std::vector< unsigned >& iargs, unsigned depth ) { - if( d_value!=val_none ){ - if( d_value==val_unk ){ - return Node::null(); - }else{ - const RepSet* rs = m->getRepSet(); - Assert(d_value >= 0 && d_value < (int)rs->getNumRepresentatives(retTyp)); - return rs->getRepresentative(retTyp, d_value); - } - }else{ - std::map< unsigned, AbsDef >::iterator it = d_def.find( iargs[depth] ); - if( it==d_def.end() ){ - return d_def[d_default].evaluate( m, retTyp, iargs, depth+1 ); - }else{ - return it->second.evaluate( m, retTyp, iargs, depth+1 ); - } - } -} - -bool AbsDef::is_normalized() { - for( std::map< unsigned, AbsDef >::iterator it1 = d_def.begin(); it1 != d_def.end(); ++it1 ){ - if( !it1->second.is_normalized() ){ - return false; - } - for( std::map< unsigned, AbsDef >::iterator it2 = d_def.begin(); it2 != d_def.end(); ++it2 ){ - if( it1->first!=it2->first && (( it1->first & it2->first )!=0) ){ - return false; - } - } - } - return true; -} - -AbsMbqiBuilder::AbsMbqiBuilder( context::Context* c, QuantifiersEngine* qe ) : -QModelBuilder( c, qe ){ - d_true = NodeManager::currentNM()->mkConst( true ); - d_false = NodeManager::currentNM()->mkConst( false ); -} - - -//------------------------model construction---------------------------- - -bool AbsMbqiBuilder::processBuildModel(TheoryModel* m) { - if (!m->areFunctionValuesEnabled()) - { - // nothing to do if no functions - return true; - } - Trace("ambqi-debug") << "process build model " << std::endl; - FirstOrderModel* f = (FirstOrderModel*)m; - FirstOrderModelAbs* fm = f->asFirstOrderModelAbs(); - RepSet* rs = m->getRepSetPtr(); - fm->initialize(); - //process representatives - fm->d_rep_id.clear(); - fm->d_domain.clear(); - - //initialize boolean sort - TypeNode b = d_true.getType(); - rs->d_type_reps[b].clear(); - rs->d_type_reps[b].push_back(d_false); - rs->d_type_reps[b].push_back(d_true); - fm->d_rep_id[d_false] = 0; - fm->d_rep_id[d_true] = 1; - - //initialize unintpreted sorts - Trace("ambqi-model") << std::endl << "Making representatives..." << std::endl; - for (std::map<TypeNode, std::vector<Node> >::iterator it = - rs->d_type_reps.begin(); - it != rs->d_type_reps.end(); - ++it) - { - if( it->first.isSort() ){ - Assert( !it->second.empty() ); - //set the domain - fm->d_domain[it->first] = 0; - Trace("ambqi-model") << "Representatives for " << it->first << " : " << std::endl; - for( unsigned i=0; i<it->second.size(); i++ ){ - if( i<32 ){ - fm->d_domain[it->first] |= ( 1 << i ); - } - Trace("ambqi-model") << i << " : " << it->second[i] << std::endl; - fm->d_rep_id[it->second[i]] = i; - } - if( it->second.size()>=32 ){ - fm->d_domain.erase( it->first ); - } - } - } - - Trace("ambqi-model") << std::endl << "Making function definitions..." << std::endl; - //construct the models for functions - for( std::map<Node, AbsDef * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) { - Node f = it->first; - Trace("ambqi-model-debug") << "Building Model for " << f << std::endl; - //reset the model - it->second->clear(); - //get all (non-redundant) f-applications - std::vector< TNode > fapps; - Trace("ambqi-model-debug") << "Initial terms: " << std::endl; - std::map< Node, std::vector< Node > >::iterator itut = fm->d_uf_terms.find( f ); - if( itut!=fm->d_uf_terms.end() ){ - for( size_t i=0; i<itut->second.size(); i++ ){ - Node n = itut->second[i]; - // only consider unique up to congruence (in model equality engine)? - Trace("ambqi-model-debug") << " " << n << " -> " << fm->getRepresentativeId( n ) << std::endl; - fapps.push_back( n ); - } - } - if( fapps.empty() ){ - //choose arbitrary value - Node mbt = fm->getModelBasisOpTerm(f); - Trace("ambqi-model-debug") << "Initial terms empty, add " << mbt << std::endl; - fapps.push_back( mbt ); - } - bool fValid = true; - for( unsigned i=0; i<fapps[0].getNumChildren(); i++ ){ - if( fm->d_domain.find( fapps[0][i].getType() )==fm->d_domain.end() ){ - Trace("ambqi-model") << "Interpretation of " << f << " is not valid."; - Trace("ambqi-model") << " (domain for " << fapps[0][i].getType() << " is too large)." << std::endl; - fValid = false; - break; - } - } - fm->d_models_valid[f] = fValid; - if( fValid ){ - //construct the ambqi model - it->second->construct_func( fm, fapps ); - Trace("ambqi-model-debug") << "Interpretation of " << f << " : " << std::endl; - it->second->debugPrint("ambqi-model-debug", fm, fapps[0] ); - Trace("ambqi-model-debug") << "Simplifying " << f << "..." << std::endl; - it->second->simplify( fm, TNode::null(), fapps[0] ); - Trace("ambqi-model") << "(Simplified) interpretation of " << f << " : " << std::endl; - it->second->debugPrint("ambqi-model", fm, fapps[0] ); - -/* - if( Debug.isOn("ambqi-model-debug") ){ - for( size_t i=0; i<fm->d_uf_terms[f].size(); i++ ){ - Node e = it->second->evaluate_n( fm, fm->d_uf_terms[f][i] ); - Debug("ambqi-model-debug") << fm->d_uf_terms[f][i] << " evaluates to " << e << std::endl; - Assert( fm->areEqual( e, fm->d_uf_terms[f][i] ) ); - } - } -*/ - } - } - Trace("ambqi-model") << "Construct model representation..." << std::endl; - //make function values - for( std::map<Node, AbsDef * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) { - if( it->first.getType().getNumChildren()>1 ){ - Trace("ambqi-model") << "Construct for " << it->first << "..." << std::endl; - Node f_def = fm->getFunctionValue( it->first, "$x" ); - m->assignFunctionDefinition( it->first, f_def ); - } - } - Assert( d_addedLemmas==0 ); - return TheoryEngineModelBuilder::processBuildModel( m ); -} - - -//--------------------model checking--------------------------------------- - -//do exhaustive instantiation -int AbsMbqiBuilder::doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort ) { - Trace("ambqi-check") << "Exhaustive instantiation " << q << " " << effort << std::endl; - if (effort==0) { - FirstOrderModelAbs * fma = fm->asFirstOrderModelAbs(); - bool quantValid = true; - for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ - if( !fma->isValidType( q[0][i].getType() ) ){ - quantValid = false; - Trace("ambqi-inst") << "Interpretation of " << q << " is not valid because of type " << q[0][i].getType() << std::endl; - break; - } - } - if( quantValid ){ - Trace("ambqi-check") << "Compute interpretation..." << std::endl; - AbsDef ad; - doCheck( fma, q, ad, q[1] ); - //now process entries - Trace("ambqi-inst-debug") << "...Current : " << d_addedLemmas << std::endl; - Trace("ambqi-inst") << "Interpretation of " << q << " is : " << std::endl; - ad.debugPrint( "ambqi-inst", fma, q[0] ); - Trace("ambqi-inst") << std::endl; - Trace("ambqi-check") << "Add instantiations..." << std::endl; - int lem = 0; - quantValid = ad.addInstantiations( fma, d_qe, q, lem ); - Trace("ambqi-inst") << "...Added " << lem << " lemmas." << std::endl; - if( lem>0 ){ - //if we were incomplete but added at least one lemma, we are ok - quantValid = true; - } - d_addedLemmas += lem; - Trace("ambqi-inst-debug") << "...Total : " << d_addedLemmas << std::endl; - } - return quantValid ? 1 : 0; - }else{ - return 1; - } -} - -bool AbsMbqiBuilder::doCheck( FirstOrderModelAbs * m, TNode q, AbsDef & ad, TNode n ) { - Assert( n.getKind()!=FORALL ); - if( n.getKind()==NOT && n[0].getKind()!=FORALL ){ - doCheck( m, q, ad, n[0] ); - ad.negate(); - return true; - }else{ - std::map< unsigned, AbsDef > children; - std::map< unsigned, int > bchildren; - std::map< unsigned, int > vchildren; - int varChCount = 0; - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - if( n[i].getKind()==FORALL ){ - bchildren[i] = AbsDef::val_unk; - }else if( n[i].getKind() == BOUND_VARIABLE ){ - varChCount++; - vchildren[i] = m->d_var_index[q][ m->getVariableId( q, n[i] ) ]; - //vchildren[i] = m->getVariableId( q, n[i] ); - }else if( m->hasTerm( n[i] ) ){ - bchildren[i] = m->getRepresentativeId( n[i] ); - }else{ - if( !doCheck( m, q, children[i], n[i] ) ){ - bchildren[i] = AbsDef::val_unk; - children.erase( i ); - } - } - } - //convert to pointers - std::map< unsigned, AbsDef * > pchildren; - for( std::map< unsigned, AbsDef >::iterator it = children.begin(); it != children.end(); ++it ){ - pchildren[it->first] = &it->second; - } - //construct the interpretation - Trace("ambqi-check-debug") << "Compute Interpretation of " << n << " " << n.getKind() << std::endl; - if( n.getKind() == APPLY_UF || n.getKind() == VARIABLE || n.getKind() == SKOLEM ){ - Node op; - if( n.getKind() == APPLY_UF ){ - op = n.getOperator(); - }else{ - op = n; - } - //uninterpreted compose - if( m->d_models_valid[op] ){ - ad.construct( m, q, n, m->d_models[op], pchildren, bchildren, vchildren, varChCount ); - }else{ - Trace("ambqi-check-debug") << "** Cannot produce interpretation for " << n << " (no function model)" << std::endl; - return false; - } - }else if( !ad.construct( m, q, n, NULL, pchildren, bchildren, vchildren, varChCount ) ){ - Trace("ambqi-check-debug") << "** Cannot produce interpretation for " << n << " (variables are children of interpreted symbol)" << std::endl; - return false; - } - Trace("ambqi-check-try") << "Interpretation for " << n << " is : " << std::endl; - ad.debugPrint("ambqi-check-try", m, q[0] ); - ad.simplify( m, q, q[0] ); - Trace("ambqi-check-debug") << "(Simplified) Interpretation for " << n << " is : " << std::endl; - ad.debugPrint("ambqi-check-debug", m, q[0] ); - Trace("ambqi-check-debug") << std::endl; - return true; - } -} - -}/* namespace CVC4::theory::quantifiers */ -}/* namespace CVC4::theory */ -}/* namespace CVC4 */ diff --git a/src/theory/quantifiers/fmf/ambqi_builder.h b/src/theory/quantifiers/fmf/ambqi_builder.h deleted file mode 100644 index b052e0985..000000000 --- a/src/theory/quantifiers/fmf/ambqi_builder.h +++ /dev/null @@ -1,105 +0,0 @@ -/********************* */ -/*! \file ambqi_builder.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Abstract MBQI model builder class - **/ - -#include "cvc4_private.h" - -#ifndef ABSTRACT_MBQI_BUILDER -#define ABSTRACT_MBQI_BUILDER - -#include "theory/quantifiers/fmf/model_builder.h" -#include "theory/quantifiers/first_order_model.h" - -namespace CVC4 { -namespace theory { -namespace quantifiers { - -class FirstOrderModelAbs; - -//representiation of function and term interpretations -class AbsDef -{ -private: - bool addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe, TNode q, std::vector< Node >& terms, int& inst, unsigned depth ); - void construct_compose( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef * f, - std::map< unsigned, AbsDef * >& children, - std::map< unsigned, int >& bchildren, std::map< unsigned, int >& vchildren, - std::vector< unsigned >& entry, std::vector< bool >& entry_def ); - void construct_entry( std::vector< unsigned >& entry, std::vector< bool >& entry_def, int v, unsigned depth = 0 ); - void construct_def_entry( FirstOrderModelAbs * m, TNode q, TNode n, int v, unsigned depth = 0 ); - void apply_ucompose( FirstOrderModelAbs * m, TNode q, - std::vector< unsigned >& entry, std::vector< bool >& entry_def, std::vector< int >& terms, - std::map< unsigned, int >& vchildren, AbsDef * a, unsigned depth = 0 ); - void construct_var_eq( FirstOrderModelAbs * m, TNode q, unsigned v1, unsigned v2, int curr, int currv, unsigned depth = 0 ); - void construct_var( FirstOrderModelAbs * m, TNode q, unsigned v, int currv, unsigned depth = 0 ); - void get_defs( unsigned u, std::vector< AbsDef * >& defs ); - void construct_normalize( FirstOrderModelAbs * m, TNode q, std::vector< AbsDef * >& defs, unsigned depth = 0 ); -public: - enum { - val_none = -1, - val_unk = -2, - }; - AbsDef() : d_default( 0 ), d_value( -1 ){} - std::map< unsigned, AbsDef > d_def; - unsigned d_default; - int d_value; - - void clear() { d_def.clear(); d_default = 0; d_value = -1; } - AbsDef * getDefault() { return &d_def[d_default]; } - void construct_func( FirstOrderModelAbs * m, std::vector< TNode >& fapps, unsigned depth = 0 ); - void debugPrintUInt( const char * c, unsigned dSize, unsigned u ) const; - void debugPrint( const char * c, FirstOrderModelAbs * m, TNode f, unsigned depth = 0 ) const; - void simplify( FirstOrderModelAbs * m, TNode q, TNode n, unsigned depth = 0 ); - int addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe, Node q, int& inst ){ - std::vector< Node > terms; - terms.resize( q[0].getNumChildren() ); - return addInstantiations( m, qe, q, terms, inst, 0 ); - } - bool construct( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef * f, - std::map< unsigned, AbsDef * >& children, - std::map< unsigned, int >& bchildren, - std::map< unsigned, int >& vchildren, - int varChCount ); - void negate(); - Node getFunctionValue( FirstOrderModelAbs * m, TNode op, std::vector< Node >& vars, unsigned depth = 0 ); - static bool isSimple( unsigned n ); - static unsigned getId( unsigned n, unsigned start=0, unsigned end=32 ); - Node evaluate( FirstOrderModelAbs * m, TypeNode retType, std::vector< Node >& args ); - Node evaluate( FirstOrderModelAbs * m, TypeNode retType, std::vector< unsigned >& iargs, unsigned depth = 0 ); - //for debugging - bool is_normalized(); -}; - -class AbsMbqiBuilder : public QModelBuilder -{ - friend class AbsDef; -private: - Node d_true; - Node d_false; - bool doCheck( FirstOrderModelAbs * m, TNode q, AbsDef & ad, TNode n ); -public: - AbsMbqiBuilder( context::Context* c, QuantifiersEngine* qe ); - - //process build model - bool processBuildModel(TheoryModel* m) override; - //do exhaustive instantiation - int doExhaustiveInstantiation(FirstOrderModel* fm, - Node q, - int effort) override; -}; - -} -} -} - -#endif diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp index c03fc7a32..8ef30fc4d 100644 --- a/src/theory/quantifiers/fmf/model_builder.cpp +++ b/src/theory/quantifiers/fmf/model_builder.cpp @@ -143,687 +143,3 @@ void QModelBuilder::debugModel( TheoryModel* m ){ } } } - -bool TermArgBasisTrie::addTerm(FirstOrderModel* fm, Node n, unsigned argIndex) -{ - if (argIndex < n.getNumChildren()) - { - Node r; - if( n[ argIndex ].getAttribute(ModelBasisAttribute()) ){ - r = n[ argIndex ]; - }else{ - r = fm->getRepresentative( n[ argIndex ] ); - } - std::map< Node, TermArgBasisTrie >::iterator it = d_data.find( r ); - if( it==d_data.end() ){ - d_data[r].addTerm(fm, n, argIndex + 1); - return true; - }else{ - return it->second.addTerm(fm, n, argIndex + 1); - } - }else{ - return false; - } -} - -void QModelBuilderIG::UfModelPreferenceData::setValuePreference(Node q, - Node r, - bool isPro) -{ - if (std::find(d_values.begin(), d_values.end(), r) == d_values.end()) - { - d_values.push_back(r); - } - int index = isPro ? 0 : 1; - if (std::find( - d_value_pro_con[index][r].begin(), d_value_pro_con[index][r].end(), q) - == d_value_pro_con[index][r].end()) - { - d_value_pro_con[index][r].push_back(q); - } -} - -Node QModelBuilderIG::UfModelPreferenceData::getBestDefaultValue( - Node defaultTerm, TheoryModel* m) -{ - Node defaultVal; - double maxScore = -1; - for (size_t i = 0, size = d_values.size(); i < size; i++) - { - Node v = d_values[i]; - double score = (1.0 + static_cast<double>(d_value_pro_con[0][v].size())) - / (1.0 + static_cast<double>(d_value_pro_con[1][v].size())); - Debug("fmf-model-cons-debug") << " - score( "; - Debug("fmf-model-cons-debug") << m->getRepresentative(v); - Debug("fmf-model-cons-debug") << " ) = " << score << std::endl; - if (score > maxScore) - { - defaultVal = v; - maxScore = score; - } - } - if (maxScore < 1.0) - { - // consider finding another value, if possible - Debug("fmf-model-cons-debug") - << "Poor choice for default value, score = " << maxScore << std::endl; - TypeNode tn = defaultTerm.getType(); - Node newDefaultVal = m->getRepSet()->getDomainValue(tn, d_values); - if (!newDefaultVal.isNull()) - { - defaultVal = newDefaultVal; - Debug("fmf-model-cons-debug") << "-> Change default value to "; - Debug("fmf-model-cons-debug") << m->getRepresentative(defaultVal); - Debug("fmf-model-cons-debug") << std::endl; - } - else - { - Debug("fmf-model-cons-debug") - << "-> Could not find arbitrary element of type " - << tn[tn.getNumChildren() - 1] << std::endl; - Debug("fmf-model-cons-debug") << " Excluding: " << d_values; - Debug("fmf-model-cons-debug") << std::endl; - } - } - // get the default term (this term must be defined non-ground in model) - Debug("fmf-model-cons-debug") << " Choose "; - Debug("fmf-model-cons-debug") << m->getRepresentative(defaultVal); - Debug("fmf-model-cons-debug") - << " as default value (" << defaultTerm << ")" << std::endl; - Debug("fmf-model-cons-debug") - << " # quantifiers pro = " << d_value_pro_con[0][defaultVal].size() - << std::endl; - Debug("fmf-model-cons-debug") - << " # quantifiers con = " << d_value_pro_con[1][defaultVal].size() - << std::endl; - return defaultVal; -} - -QModelBuilderIG::QModelBuilderIG(context::Context* c, QuantifiersEngine* qe) - : QModelBuilder(c, qe), - d_didInstGen(false), - d_numQuantSat(0), - d_numQuantInstGen(0), - d_numQuantNoInstGen(0), - d_numQuantNoSelForm(0), - d_instGenMatches(0) {} - -/* -Node QModelBuilderIG::getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::vector< Node > & args, bool partial ) { - return n; -} -*/ - -bool QModelBuilderIG::processBuildModel( TheoryModel* m ) { - if (!m->areFunctionValuesEnabled()) - { - // nothing to do if no functions - return true; - } - FirstOrderModel* f = (FirstOrderModel*)m; - FirstOrderModelIG* fm = f->asFirstOrderModelIG(); - Trace("model-engine-debug") << "Process build model " << optUseModel() << std::endl; - d_didInstGen = false; - //reset the internal information - reset( fm ); - //only construct first order model if optUseModel() is true - if( optUseModel() ){ - Trace("model-engine-debug") << "Initializing " << fm->getNumAssertedQuantifiers() << " quantifiers..." << std::endl; - //check if any quantifiers are un-initialized - for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ - Node q = fm->getAssertedQuantifier( i ); - if( d_qe->getModel()->isQuantifierActive( q ) ){ - int lems = initializeQuantifier(q, q, f); - d_statistics.d_init_inst_gen_lemmas += lems; - d_addedLemmas += lems; - if( d_qe->inConflict() ){ - break; - } - } - } - if( d_addedLemmas>0 ){ - Trace("model-engine") << "Initialize, Added Lemmas = " << d_addedLemmas << std::endl; - return false; - }else{ - Assert( !d_qe->inConflict() ); - //initialize model - fm->initialize(); - //analyze the functions - Trace("model-engine-debug") << "Analyzing model..." << std::endl; - analyzeModel( fm ); - //analyze the quantifiers - Trace("model-engine-debug") << "Analyzing quantifiers..." << std::endl; - d_uf_prefs.clear(); - for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ - Node q = fm->getAssertedQuantifier( i ); - analyzeQuantifier( fm, q ); - } - - //if applicable, find exceptions to model via inst-gen - if( options::fmfInstGen() ){ - d_didInstGen = true; - d_instGenMatches = 0; - d_numQuantSat = 0; - d_numQuantInstGen = 0; - d_numQuantNoInstGen = 0; - d_numQuantNoSelForm = 0; - //now, see if we know that any exceptions via InstGen exist - Trace("model-engine-debug") << "Perform InstGen techniques for quantifiers..." << std::endl; - for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ - Node f = fm->getAssertedQuantifier( i ); - if( d_qe->getModel()->isQuantifierActive( f ) ){ - int lems = doInstGen( fm, f ); - d_statistics.d_inst_gen_lemmas += lems; - d_addedLemmas += lems; - //temporary - if( lems>0 ){ - d_numQuantInstGen++; - }else if( hasInstGen( f ) ){ - d_numQuantNoInstGen++; - }else{ - d_numQuantNoSelForm++; - } - if( d_qe->inConflict() || ( options::fmfInstGenOneQuantPerRound() && lems>0 ) ){ - break; - } - }else{ - d_numQuantSat++; - } - } - Trace("model-engine-debug") << "Quantifiers sat/ig/n-ig/null " << d_numQuantSat << " / " << d_numQuantInstGen << " / "; - Trace("model-engine-debug") << d_numQuantNoInstGen << " / " << d_numQuantNoSelForm << std::endl; - Trace("model-engine-debug") << "Inst-gen # matches examined = " << d_instGenMatches << std::endl; - if( Trace.isOn("model-engine") ){ - if( d_addedLemmas>0 ){ - Trace("model-engine") << "InstGen, added lemmas = " << d_addedLemmas << std::endl; - }else{ - Trace("model-engine") << "No InstGen lemmas..." << std::endl; - } - } - } - //construct the model if necessary - if( d_addedLemmas==0 ){ - //if no immediate exceptions, build the model - // this model will be an approximation that will need to be tested via exhaustive instantiation - Trace("model-engine-debug") << "Building model..." << std::endl; - //build model for UF - for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){ - Trace("model-engine-debug-uf") << "Building model for " << it->first << "..." << std::endl; - constructModelUf( fm, it->first ); - } - Trace("model-engine-debug") << "Done building models." << std::endl; - }else{ - return false; - } - } - } - //update models - for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){ - it->second.update( fm ); - Trace("model-func") << "QModelBuilder: Make function value from tree " << it->first << std::endl; - //construct function values - Node f_def = it->second.getFunctionValue( "$x" ); - fm->assignFunctionDefinition( it->first, f_def ); - } - Assert( d_addedLemmas==0 ); - return TheoryEngineModelBuilder::processBuildModel( m ); -} - -int QModelBuilderIG::initializeQuantifier(Node f, Node fp, FirstOrderModel* fm) -{ - if( d_quant_basis_match_added.find( f )==d_quant_basis_match_added.end() ){ - //create the basis match if necessary - if( d_quant_basis_match.find( f )==d_quant_basis_match.end() ){ - Trace("inst-fmf-init") << "Initialize " << f << std::endl; - //add the model basis instantiation - // This will help produce the necessary information for model completion. - // We do this by extending distinguish ground assertions (those - // containing terms with "model basis" attribute) to hold for all cases. - - ////first, check if any variables are required to be equal - //for( std::map< Node, bool >::iterator it = d_quantEngine->d_phase_reqs[f].begin(); - // it != d_quantEngine->d_phase_reqs[f].end(); ++it ){ - // Node n = it->first; - // if( n.getKind()==EQUAL && n[0].getKind()==INST_CONSTANT && n[1].getKind()==INST_CONSTANT ){ - // Notice() << "Unhandled phase req: " << n << std::endl; - // } - //} - d_quant_basis_match[f] = InstMatch( f ); - for (unsigned j = 0; j < f[0].getNumChildren(); j++) - { - Node t = fm->getModelBasisTerm(f[0][j].getType()); - //calculate the basis match for f - d_quant_basis_match[f].setValue( j, t ); - } - ++(d_statistics.d_num_quants_init); - } - //try to add it - Trace("inst-fmf-init") << "Init: try to add match " << d_quant_basis_match[f] << std::endl; - //add model basis instantiation - if (d_qe->getInstantiate()->addInstantiation(fp, d_quant_basis_match[f])) - { - d_quant_basis_match_added[f] = true; - return 1; - }else{ - //shouldn't happen usually, but will occur if x != y is a required literal for f. - //Notice() << "No model basis for " << f << std::endl; - d_quant_basis_match_added[f] = false; - } - } - return 0; -} - -void QModelBuilderIG::analyzeModel( FirstOrderModel* fm ){ - FirstOrderModelIG* fmig = fm->asFirstOrderModelIG(); - d_uf_model_constructed.clear(); - //determine if any functions are constant - for( std::map< Node, uf::UfModelTree >::iterator it = fmig->d_uf_model_tree.begin(); it != fmig->d_uf_model_tree.end(); ++it ){ - Node op = it->first; - std::map< Node, std::vector< Node > >::iterator itut = fmig->d_uf_terms.find( op ); - if( itut!=fmig->d_uf_terms.end() ){ - for( size_t i=0; i<itut->second.size(); i++ ){ - Node n = fmig->d_uf_terms[op][i]; - //for calculating if op is constant - Node v = fmig->getRepresentative( n ); - if( i==0 ){ - d_uf_prefs[op].d_const_val = v; - }else if( v!=d_uf_prefs[op].d_const_val ){ - d_uf_prefs[op].d_const_val = Node::null(); - break; - } - } - } - if( !d_uf_prefs[op].d_const_val.isNull() ){ - fmig->d_uf_model_gen[op].setDefaultValue( d_uf_prefs[op].d_const_val ); - fmig->d_uf_model_gen[op].makeModel( fmig, it->second ); - Debug("fmf-model-cons") << "Function " << op << " is the constant function "; - Debug("fmf-model-cons") << d_uf_prefs[op].d_const_val; - Debug("fmf-model-cons") << std::endl; - d_uf_model_constructed[op] = true; - }else{ - d_uf_model_constructed[op] = false; - } - } -} - -bool QModelBuilderIG::hasConstantDefinition( Node n ){ - Node lit = n.getKind()==NOT ? n[0] : n; - if( lit.getKind()==APPLY_UF ){ - Node op = lit.getOperator(); - if( !d_uf_prefs[op].d_const_val.isNull() ){ - return true; - } - } - return false; -} - -QModelBuilderIG::Statistics::Statistics() - : d_num_quants_init("QModelBuilderIG::Number_Quantifiers", 0), - d_num_partial_quants_init("QModelBuilderIG::Number_Partial_Quantifiers", - 0), - d_init_inst_gen_lemmas("QModelBuilderIG::Initialize_Inst_Gen_Lemmas", 0), - d_inst_gen_lemmas("QModelBuilderIG::Inst_Gen_Lemmas", 0) -{ - smtStatisticsRegistry()->registerStat(&d_num_quants_init); - smtStatisticsRegistry()->registerStat(&d_num_partial_quants_init); - smtStatisticsRegistry()->registerStat(&d_init_inst_gen_lemmas); - smtStatisticsRegistry()->registerStat(&d_inst_gen_lemmas); -} - -QModelBuilderIG::Statistics::~Statistics(){ - smtStatisticsRegistry()->unregisterStat(&d_num_quants_init); - smtStatisticsRegistry()->unregisterStat(&d_num_partial_quants_init); - smtStatisticsRegistry()->unregisterStat(&d_init_inst_gen_lemmas); - smtStatisticsRegistry()->unregisterStat(&d_inst_gen_lemmas); -} - -//do exhaustive instantiation -int QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { - if( optUseModel() ){ - QRepBoundExt qrbe(d_qe); - RepSetIterator riter(d_qe->getModel()->getRepSet(), &qrbe); - if( riter.setQuantifier( f ) ){ - FirstOrderModelIG * fmig = (FirstOrderModelIG*)d_qe->getModel(); - Debug("inst-fmf-ei") << "Reset evaluate..." << std::endl; - fmig->resetEvaluate(); - Debug("inst-fmf-ei") << "Begin instantiation..." << std::endl; - EqualityQuery* qy = d_qe->getEqualityQuery(); - Instantiate* inst = d_qe->getInstantiate(); - TermUtil* util = d_qe->getTermUtil(); - while( !riter.isFinished() && ( d_addedLemmas==0 || !options::fmfOneInstPerRound() ) ){ - d_triedLemmas++; - if( Debug.isOn("inst-fmf-ei-debug") ){ - for( int i=0; i<(int)riter.d_index.size(); i++ ){ - Debug("inst-fmf-ei-debug") << i << " : " << riter.d_index[i] << " : " << riter.getCurrentTerm( i ) << std::endl; - } - } - int eval = 0; - int depIndex; - //see if instantiation is already true in current model - if( Debug.isOn("fmf-model-eval") ){ - Debug("fmf-model-eval") << "Evaluating "; - riter.debugPrintSmall("fmf-model-eval"); - Debug("fmf-model-eval") << "Done calculating terms." << std::endl; - } - //if evaluate(...)==1, then the instantiation is already true in the model - // depIndex is the index of the least significant variable that this evaluation relies upon - depIndex = riter.getNumTerms()-1; - Debug("fmf-model-eval") << "We will evaluate " - << util->getInstConstantBody(f) << std::endl; - eval = fmig->evaluate(util->getInstConstantBody(f), depIndex, &riter); - if( eval==1 ){ - Debug("fmf-model-eval") << " Returned success with depIndex = " << depIndex << std::endl; - }else{ - Debug("fmf-model-eval") << " Returned " << (eval==-1 ? "failure" : "unknown") << ", depIndex = " << depIndex << std::endl; - } - if( eval==1 ){ - //instantiation is already true -> skip - riter.incrementAtIndex(depIndex); - }else{ - //instantiation was not shown to be true, construct the match - InstMatch m( f ); - for (unsigned i = 0; i < riter.getNumTerms(); i++) - { - m.set(qy, i, riter.getCurrentTerm(i)); - } - Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl; - //add as instantiation - if (inst->addInstantiation(f, m, true)) - { - d_addedLemmas++; - if( d_qe->inConflict() ){ - break; - } - //if the instantiation is show to be false, and we wish to skip multiple instantiations at once - if( eval==-1 ){ - riter.incrementAtIndex(depIndex); - }else{ - riter.increment(); - } - }else{ - Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl; - riter.increment(); - } - } - } - //print debugging information - Trace("inst-fmf-ei") << "For " << f << ", finished: " << std::endl; - Trace("inst-fmf-ei") << " Inst Tried: " << d_triedLemmas << std::endl; - Trace("inst-fmf-ei") << " Inst Added: " << d_addedLemmas << std::endl; - if( d_addedLemmas>1000 ){ - Trace("model-engine-warn") << "WARNING: many instantiations produced for " << f << ": " << std::endl; - Trace("model-engine-warn") << " Inst Tried: " << d_triedLemmas << std::endl; - Trace("model-engine-warn") << " Inst Added: " << d_addedLemmas << std::endl; - Trace("model-engine-warn") << std::endl; - } - } - //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round - return riter.isIncomplete() ? -1 : 1; - }else{ - return 0; - } -} - - - -void QModelBuilderDefault::reset( FirstOrderModel* fm ){ - d_quant_selection_lit.clear(); - d_quant_selection_lit_candidates.clear(); - d_quant_selection_lit_terms.clear(); - d_term_selection_lit.clear(); - d_op_selection_terms.clear(); -} - - -int QModelBuilderDefault::getSelectionScore( std::vector< Node >& uf_terms ) { - /* - size_t maxChildren = 0; - for( size_t i=0; i<uf_terms.size(); i++ ){ - if( uf_terms[i].getNumChildren()>maxChildren ){ - maxChildren = uf_terms[i].getNumChildren(); - } - } - //TODO: look at how many entries they have? - return (int)maxChildren; - */ - return 0; -} - -void QModelBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ){ - if( d_qe->getModel()->isQuantifierActive( f ) ){ - FirstOrderModelIG* fmig = fm->asFirstOrderModelIG(); - Debug("fmf-model-prefs") << "Analyze quantifier " << f << std::endl; - //the pro/con preferences for this quantifier - std::vector< Node > pro_con[2]; - //the terms in the selection literal we choose - std::vector< Node > selectionLitTerms; - Trace("inst-gen-debug-quant") << "Inst-gen analyze " << f << std::endl; - //for each asserted quantifier f, - // - determine selection literals - // - check which function/predicates have good and bad definitions for satisfying f - if( d_phase_reqs.find( f )==d_phase_reqs.end() ){ - d_phase_reqs[f].initialize( d_qe->getTermUtil()->getInstConstantBody( f ), true ); - } - int selectLitScore = -1; - for( std::map< Node, bool >::iterator it = d_phase_reqs[f].d_phase_reqs.begin(); it != d_phase_reqs[f].d_phase_reqs.end(); ++it ){ - //the literal n is phase-required for quantifier f - Node n = it->first; - Node gn = fm->getModelBasis(f, n); - Debug("fmf-model-req") << " Req: " << n << " -> " << it->second << std::endl; - bool value; - //if the corresponding ground abstraction literal has a SAT value - if( d_qe->getValuation().hasSatValue( gn, value ) ){ - //collect the non-ground uf terms that this literal contains - // and compute if all of the symbols in this literal have - // constant definitions. - bool isConst = true; - std::vector< Node > uf_terms; - if( TermUtil::hasInstConstAttr(n) ){ - isConst = false; - if( gn.getKind()==APPLY_UF ){ - uf_terms.push_back( gn ); - isConst = hasConstantDefinition( gn ); - }else if( gn.getKind()==EQUAL ){ - isConst = true; - for( int j=0; j<2; j++ ){ - if( TermUtil::hasInstConstAttr(n[j]) ){ - if( n[j].getKind()==APPLY_UF && - fmig->d_uf_model_tree.find( gn[j].getOperator() )!=fmig->d_uf_model_tree.end() ){ - uf_terms.push_back( gn[j] ); - isConst = isConst && hasConstantDefinition( gn[j] ); - }else{ - isConst = false; - } - } - } - } - } - //check if the value in the SAT solver matches the preference according to the quantifier - int pref = 0; - if( value!=it->second ){ - //we have a possible selection literal - bool selectLit = d_quant_selection_lit[f].isNull(); - bool selectLitConstraints = true; - //it is a constantly defined selection literal : the quantifier is sat - if( isConst ){ - selectLit = selectLit || d_qe->getModel()->isQuantifierActive( f ); - d_qe->getModel()->setQuantifierActive( f, false ); - //check if choosing this literal would add any additional constraints to default definitions - selectLitConstraints = false; - selectLit = true; - } - //also check if it is naturally a better literal - if( !selectLit ){ - int score = getSelectionScore( uf_terms ); - //Trace("inst-gen-debug") << "Check " << score << " < " << selectLitScore << std::endl; - selectLit = score<selectLitScore; - } - //see if we wish to choose this as a selection literal - d_quant_selection_lit_candidates[f].push_back( value ? n : n.notNode() ); - if( selectLit ){ - selectLitScore = getSelectionScore( uf_terms ); - Trace("inst-gen-debug") << "Choose selection literal " << gn << std::endl; - Trace("inst-gen-debug") << " flags: " << isConst << " " << selectLitConstraints << " " << selectLitScore << std::endl; - d_quant_selection_lit[f] = value ? n : n.notNode(); - selectionLitTerms.clear(); - selectionLitTerms.insert( selectionLitTerms.begin(), uf_terms.begin(), uf_terms.end() ); - if( !selectLitConstraints ){ - break; - } - } - pref = 1; - }else{ - pref = -1; - } - //if we are not yet SAT, so we will add to preferences - if( d_qe->getModel()->isQuantifierActive( f ) ){ - Debug("fmf-model-prefs") << " It is " << ( pref==1 ? "pro" : "con" ); - Debug("fmf-model-prefs") << " the definition of " << n << std::endl; - for( int j=0; j<(int)uf_terms.size(); j++ ){ - pro_con[ pref==1 ? 0 : 1 ].push_back( uf_terms[j] ); - } - } - } - } - //process information about selection literal for f - if( !d_quant_selection_lit[f].isNull() ){ - d_quant_selection_lit_terms[f].insert( d_quant_selection_lit_terms[f].begin(), selectionLitTerms.begin(), selectionLitTerms.end() ); - for( int i=0; i<(int)selectionLitTerms.size(); i++ ){ - d_term_selection_lit[ selectionLitTerms[i] ] = d_quant_selection_lit[f]; - d_op_selection_terms[ selectionLitTerms[i].getOperator() ].push_back( selectionLitTerms[i] ); - } - }else{ - Trace("inst-gen-warn") << "WARNING: " << f << " has no selection literals" << std::endl; - } - //process information about requirements and preferences of quantifier f - if( !d_qe->getModel()->isQuantifierActive( f ) ){ - Debug("fmf-model-prefs") << " * Constant SAT due to definition of ops: "; - for( int i=0; i<(int)selectionLitTerms.size(); i++ ){ - Debug("fmf-model-prefs") << selectionLitTerms[i] << " "; - } - Debug("fmf-model-prefs") << std::endl; - }else{ - //note quantifier's value preferences to models - for( int k=0; k<2; k++ ){ - for( int j=0; j<(int)pro_con[k].size(); j++ ){ - Node op = pro_con[k][j].getOperator(); - Node r = fmig->getRepresentative( pro_con[k][j] ); - d_uf_prefs[op].setValuePreference(f, r, k == 0); - } - } - } - } -} - -int QModelBuilderDefault::doInstGen( FirstOrderModel* fm, Node f ){ - int addedLemmas = 0; - //we wish to add all known exceptions to our selection literal for f. this will help to refine our current model. - //This step is advantageous over exhaustive instantiation, since we are adding instantiations that involve model basis terms, - // effectively acting as partial instantiations instead of pointwise instantiations. - if( !d_quant_selection_lit[f].isNull() ){ - Trace("inst-gen") << "Do Inst-Gen for " << f << std::endl; - for( size_t i=0; i<d_quant_selection_lit_candidates[f].size(); i++ ){ - bool phase = d_quant_selection_lit_candidates[f][i].getKind()!=NOT; - Node lit = d_quant_selection_lit_candidates[f][i].getKind()==NOT ? d_quant_selection_lit_candidates[f][i][0] : d_quant_selection_lit_candidates[f][i]; - Assert( TermUtil::hasInstConstAttr(lit) ); - std::vector< Node > tr_terms; - if( lit.getKind()==APPLY_UF ){ - //only match predicates that are contrary to this one, use literal matching - Node eq = NodeManager::currentNM()->mkNode( - EQUAL, lit, NodeManager::currentNM()->mkConst(!phase)); - tr_terms.push_back( eq ); - }else if( lit.getKind()==EQUAL ){ - //collect trigger terms - for( int j=0; j<2; j++ ){ - if( TermUtil::hasInstConstAttr(lit[j]) ){ - if( lit[j].getKind()==APPLY_UF ){ - tr_terms.push_back( lit[j] ); - }else{ - tr_terms.clear(); - break; - } - } - } - if( tr_terms.size()==1 && !phase ){ - //equality between a function and a ground term, use literal matching - tr_terms.clear(); - tr_terms.push_back( lit ); - } - } - //if applicable, try to add exceptions here - if( !tr_terms.empty() ){ - //make a trigger for these terms, add instantiations - inst::Trigger* tr = inst::Trigger::mkTrigger( d_qe, f, tr_terms, true, inst::Trigger::TR_MAKE_NEW ); - //Notice() << "Trigger = " << (*tr) << std::endl; - tr->resetInstantiationRound(); - tr->reset( Node::null() ); - //d_qe->d_optInstMakeRepresentative = false; - //d_qe->d_optMatchIgnoreModelBasis = true; - addedLemmas += tr->addInstantiations(); - } - } - } - return addedLemmas; -} - -void QModelBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ){ - FirstOrderModelIG* fmig = fm->asFirstOrderModelIG(); - if( !d_uf_model_constructed[op] ){ - //construct the model for the uninterpretted function/predicate - bool setDefaultVal = true; - Node defaultTerm = fmig->getModelBasisOpTerm(op); - Trace("fmf-model-cons") << "Construct model for " << op << "..." << std::endl; - //set the values in the model - std::map< Node, std::vector< Node > >::iterator itut = fmig->d_uf_terms.find( op ); - if( itut!=fmig->d_uf_terms.end() ){ - for( size_t i=0; i<itut->second.size(); i++ ){ - Node n = itut->second[i]; - // only consider unique up to congruence (in model equality engine)? - Node v = fmig->getRepresentative( n ); - Trace("fmf-model-cons") << "Set term " << n << " : " - << fmig->getRepSet()->getIndexFor(v) << " " << v - << std::endl; - //if this assertion did not help the model, just consider it ground - //set n = v in the model tree - //set it as ground value - fmig->d_uf_model_gen[op].setValue( fm, n, v ); - // also set as default value if necessary - if (n.hasAttribute(ModelBasisArgAttribute()) - && n.getAttribute(ModelBasisArgAttribute()) != 0) - { - Trace("fmf-model-cons") << " Set as default." << std::endl; - fmig->d_uf_model_gen[op].setValue(fm, n, v, false); - if( n==defaultTerm ){ - //incidentally already set, we will not need to find a default value - setDefaultVal = false; - } - } - } - } - //set the overall default value if not set already (is this necessary??) - if( setDefaultVal ){ - Trace("fmf-model-cons") << " Choose default value..." << std::endl; - //chose defaultVal based on heuristic, currently the best ratio of "pro" responses - Node defaultVal = d_uf_prefs[op].getBestDefaultValue( defaultTerm, fm ); - if( defaultVal.isNull() ){ - if (!fmig->getRepSet()->hasType(defaultTerm.getType())) - { - Node mbt = fmig->getModelBasisTerm(defaultTerm.getType()); - fmig->getRepSetPtr()->d_type_reps[defaultTerm.getType()].push_back( - mbt); - } - defaultVal = - fmig->getRepSet()->getRepresentative(defaultTerm.getType(), 0); - } - Assert( !defaultVal.isNull() ); - Trace("fmf-model-cons") - << "Set default term : " << fmig->getRepSet()->getIndexFor(defaultVal) - << std::endl; - fmig->d_uf_model_gen[op].setValue( fm, defaultTerm, defaultVal, false ); - } - Debug("fmf-model-cons") << " Making model..."; - fmig->d_uf_model_gen[op].makeModel( fm, fmig->d_uf_model_tree[op] ); - d_uf_model_constructed[op] = true; - Debug("fmf-model-cons") << " Finished constructing model for " << op << "." << std::endl; - } -} diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h index b34f1e580..b73716169 100644 --- a/src/theory/quantifiers/fmf/model_builder.h +++ b/src/theory/quantifiers/fmf/model_builder.h @@ -56,163 +56,6 @@ public: unsigned getNumTriedLemmas() { return d_triedLemmas; } }; -class TermArgBasisTrie { -public: - /** the data */ - std::map< Node, TermArgBasisTrie > d_data; - /** add term to the trie */ - bool addTerm(FirstOrderModel* fm, Node n, unsigned argIndex = 0); -};/* class TermArgBasisTrie */ - -/** model builder class - * This class is capable of building candidate models based on the current quantified formulas - * that are asserted. Use: - * (1) call QModelBuilder::buildModel( m, false );, where m is a FirstOrderModel - * (2) if candidate model is determined to be a real model, - then call QModelBuilder::buildModel( m, true ); - */ -class QModelBuilderIG : public QModelBuilder -{ - typedef context::CDHashMap<Node, bool, NodeHashFunction> BoolMap; - - protected: - /** - * This class stores temporary information useful to model engine for - * constructing models for uninterpreted functions. - */ - class UfModelPreferenceData - { - public: - UfModelPreferenceData() {} - virtual ~UfModelPreferenceData() {} - /** any constant value of the type */ - Node d_const_val; - /** list of possible default values */ - std::vector<Node> d_values; - /** - * Map from values to the set of quantified formulas that are (pro, con) - * that value. A quantified formula may be "pro" a particular default - * value of an uninterpreted function if that value is likely to satisfy - * many points in its domain. For example, forall x. P( f( x ) ) may be - * "pro" the default value true for P. - */ - std::map<Node, std::vector<Node> > d_value_pro_con[2]; - /** set that quantified formula q is pro/con the default value of r */ - void setValuePreference(Node q, Node r, bool isPro); - /** get best default value */ - Node getBestDefaultValue(Node defaultTerm, TheoryModel* m); - }; - /** map from operators to model preference data */ - std::map<Node, UfModelPreferenceData> d_uf_prefs; - //built model uf - std::map< Node, bool > d_uf_model_constructed; - //whether inst gen was done - bool d_didInstGen; - /** process build model */ - bool processBuildModel(TheoryModel* m) override; - - protected: - //reset - virtual void reset( FirstOrderModel* fm ) = 0; - //initialize quantifiers, return number of lemmas produced - virtual int initializeQuantifier(Node f, Node fp, FirstOrderModel* fm); - //analyze model - virtual void analyzeModel( FirstOrderModel* fm ); - //analyze quantifiers - virtual void analyzeQuantifier( FirstOrderModel* fm, Node f ) = 0; - //do InstGen techniques for quantifier, return number of lemmas produced - virtual int doInstGen( FirstOrderModel* fm, Node f ) = 0; - //theory-specific build models - virtual void constructModelUf( FirstOrderModel* fm, Node op ) = 0; - - protected: - //map from quantifiers to if are SAT - //std::map< Node, bool > d_quant_sat; - //which quantifiers have been initialized - std::map< Node, bool > d_quant_basis_match_added; - //map from quantifiers to model basis match - std::map< Node, InstMatch > d_quant_basis_match; - - protected: // helper functions - /** term has constant definition */ - bool hasConstantDefinition( Node n ); - - public: - QModelBuilderIG( context::Context* c, QuantifiersEngine* qe ); - - public: - /** statistics class */ - class Statistics { - public: - IntStat d_num_quants_init; - IntStat d_num_partial_quants_init; - IntStat d_init_inst_gen_lemmas; - IntStat d_inst_gen_lemmas; - Statistics(); - ~Statistics(); - }; - Statistics d_statistics; - // is term selected - virtual bool isTermSelected( Node n ) { return false; } - /** quantifier has inst-gen definition */ - virtual bool hasInstGen( Node f ) = 0; - /** did inst gen this round? */ - bool didInstGen() { return d_didInstGen; } - // is quantifier active? - bool isQuantifierActive( Node f ); - //do exhaustive instantiation - int doExhaustiveInstantiation(FirstOrderModel* fm, - Node f, - int effort) override; - - //temporary stats - int d_numQuantSat; - int d_numQuantInstGen; - int d_numQuantNoInstGen; - int d_numQuantNoSelForm; - //temporary stat - int d_instGenMatches; -};/* class QModelBuilder */ - - -class QModelBuilderDefault : public QModelBuilderIG -{ - private: /// information for (old) InstGen - // map from quantifiers to their selection literals - std::map< Node, Node > d_quant_selection_lit; - std::map< Node, std::vector< Node > > d_quant_selection_lit_candidates; - //map from quantifiers to their selection literal terms - std::map< Node, std::vector< Node > > d_quant_selection_lit_terms; - //map from terms to the selection literals they exist in - std::map< Node, Node > d_term_selection_lit; - //map from operators to terms that appear in selection literals - std::map< Node, std::vector< Node > > d_op_selection_terms; - //get selection score - int getSelectionScore( std::vector< Node >& uf_terms ); - - protected: - //reset - void reset(FirstOrderModel* fm) override; - //analyze quantifier - void analyzeQuantifier(FirstOrderModel* fm, Node f) override; - //do InstGen techniques for quantifier, return number of lemmas produced - int doInstGen(FirstOrderModel* fm, Node f) override; - //theory-specific build models - void constructModelUf(FirstOrderModel* fm, Node op) override; - - protected: - std::map< Node, QuantPhaseReq > d_phase_reqs; - - public: - QModelBuilderDefault( context::Context* c, QuantifiersEngine* qe ) : QModelBuilderIG( c, qe ){} - - //has inst gen - bool hasInstGen(Node f) override - { - return !d_quant_selection_lit[f].isNull(); - } -}; - }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index 81ecf9e77..d2579b4ee 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -15,7 +15,6 @@ #include "theory/quantifiers/fmf/model_engine.h" #include "options/quantifiers_options.h" -#include "theory/quantifiers/fmf/ambqi_builder.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/fmf/full_model_check.h" #include "theory/quantifiers/instantiate.h" diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index d4735b3d8..aa20c1f76 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -138,159 +138,195 @@ void CegSingleInv::initialize(Node q) } } // compute single invocation partition - if( options::cegqiSingleInvMode()!=CEGQI_SI_MODE_NONE ){ - Node qq; - if( q[1].getKind()==NOT && q[1][0].getKind()==FORALL ){ - qq = q[1][0][1]; - }else{ - qq = TermUtil::simpleNegate( q[1] ); - } - //process the single invocation-ness of the property - if( !d_sip->init( progs, qq ) ){ - Trace("cegqi-si") << "...not single invocation (type mismatch)" << std::endl; - }else{ - Trace("cegqi-si") << "- Partitioned to single invocation parts : " << std::endl; - d_sip->debugPrint( "cegqi-si" ); + Node qq; + if (q[1].getKind() == NOT && q[1][0].getKind() == FORALL) + { + qq = q[1][0][1]; + } + else + { + qq = TermUtil::simpleNegate(q[1]); + } + // process the single invocation-ness of the property + if (!d_sip->init(progs, qq)) + { + Trace("cegqi-si") << "...not single invocation (type mismatch)" + << std::endl; + return; + } + Trace("cegqi-si") << "- Partitioned to single invocation parts : " + << std::endl; + d_sip->debugPrint("cegqi-si"); + + // map from program to bound variables + std::vector<Node> funcs; + d_sip->getFunctions(funcs); + for (unsigned j = 0, size = funcs.size(); j < size; j++) + { + Assert(std::find(progs.begin(), progs.end(), funcs[j]) != progs.end()); + d_prog_to_sol_index[funcs[j]] = j; + } - //map from program to bound variables - std::vector<Node> funcs; - d_sip->getFunctions(funcs); - for (unsigned j = 0, size = funcs.size(); j < size; j++) + // check if it is single invocation + if (d_sip->isPurelySingleInvocation()) + { + // We are fully single invocation, set single invocation if we haven't + // disabled single invocation techniques. + if (options::cegqiSingleInvMode() != CEGQI_SI_MODE_NONE) + { + d_single_invocation = true; + return; + } + } + // We are processing without single invocation techniques, now check if + // we should fix an invariant template (post-condition strengthening or + // pre-condition weakening). + SygusInvTemplMode tmode = options::sygusInvTemplMode(); + if (tmode != SYGUS_INV_TEMPL_MODE_NONE) + { + // currently only works for single predicate synthesis + if (q[0].getNumChildren() > 1 || !q[0][0].getType().isPredicate()) + { + tmode = SYGUS_INV_TEMPL_MODE_NONE; + } + else if (!options::sygusInvTemplWhenSyntax()) + { + // only use invariant templates if no syntactic restrictions + if (CegGrammarConstructor::hasSyntaxRestrictions(q)) { - Assert(std::find(progs.begin(), progs.end(), funcs[j]) != progs.end()); - d_prog_to_sol_index[funcs[j]] = j; + tmode = SYGUS_INV_TEMPL_MODE_NONE; } + } + } + + if (tmode == SYGUS_INV_TEMPL_MODE_NONE) + { + // not processing invariant templates + return; + } + // if we are doing invariant templates, then construct the template + Trace("cegqi-si") << "- Do transition inference..." << std::endl; + d_ti[q].process(qq); + Trace("cegqi-inv") << std::endl; + if (d_ti[q].d_func.isNull()) + { + // the invariant could not be inferred + return; + } + NodeManager* nm = NodeManager::currentNM(); + // map the program back via non-single invocation map + Node prog = d_ti[q].d_func; + std::vector<Node> prog_templ_vars; + prog_templ_vars.insert( + prog_templ_vars.end(), d_ti[q].d_vars.begin(), d_ti[q].d_vars.end()); + d_trans_pre[prog] = d_ti[q].getComponent(1); + d_trans_post[prog] = d_ti[q].getComponent(-1); + Trace("cegqi-inv") << " precondition : " << d_trans_pre[prog] << std::endl; + Trace("cegqi-inv") << " postcondition : " << d_trans_post[prog] << std::endl; + std::vector<Node> sivars; + d_sip->getSingleInvocationVariables(sivars); + Node invariant = d_sip->getFunctionInvocationFor(prog); + Assert(!invariant.isNull()); + invariant = invariant.substitute(sivars.begin(), + sivars.end(), + prog_templ_vars.begin(), + prog_templ_vars.end()); + Trace("cegqi-inv") << " invariant : " << invariant << std::endl; - //check if it is single invocation - if (!d_sip->isPurelySingleInvocation()) + // store simplified version of quantified formula + d_simp_quant = d_sip->getFullSpecification(); + std::vector<Node> new_bv; + for( const Node& v : sivars ) + { + new_bv.push_back(nm->mkBoundVar(v.getType())); + } + d_simp_quant = d_simp_quant.substitute( + sivars.begin(), sivars.end(), new_bv.begin(), new_bv.end()); + Assert(q[1].getKind() == NOT && q[1][0].getKind() == FORALL); + for (const Node& v : q[1][0][0]) + { + new_bv.push_back(v); + } + d_simp_quant = + nm->mkNode(FORALL, nm->mkNode(BOUND_VAR_LIST, new_bv), d_simp_quant) + .negate(); + d_simp_quant = Rewriter::rewrite(d_simp_quant); + d_simp_quant = nm->mkNode(FORALL, q[0], d_simp_quant, q[2]); + Trace("cegqi-si") << "Rewritten quantifier : " << d_simp_quant << std::endl; + + // construct template argument + d_templ_arg[prog] = nm->mkSkolem("I", invariant.getType()); + + // construct template + Node templ; + if (options::sygusInvAutoUnfold()) + { + if (d_ti[q].isComplete()) + { + Trace("cegqi-inv-auto-unfold") + << "Automatic deterministic unfolding... " << std::endl; + // auto-unfold + DetTrace dt; + int init_dt = d_ti[q].initializeTrace(dt); + if (init_dt == 0) { - SygusInvTemplMode tmode = options::sygusInvTemplMode(); - if (tmode != SYGUS_INV_TEMPL_MODE_NONE) + Trace("cegqi-inv-auto-unfold") << " Init : "; + dt.print("cegqi-inv-auto-unfold"); + Trace("cegqi-inv-auto-unfold") << std::endl; + unsigned counter = 0; + unsigned status = 0; + while (counter < 100 && status == 0) { - // currently only works for single predicate synthesis - if (q[0].getNumChildren() > 1 || !q[0][0].getType().isPredicate()) - { - tmode = SYGUS_INV_TEMPL_MODE_NONE; - } - else if (!options::sygusInvTemplWhenSyntax()) - { - // only use invariant templates if no syntactic restrictions - if (CegGrammarConstructor::hasSyntaxRestrictions(q)) - { - tmode = SYGUS_INV_TEMPL_MODE_NONE; - } - } + status = d_ti[q].incrementTrace(dt); + counter++; + Trace("cegqi-inv-auto-unfold") << " #" << counter << " : "; + dt.print("cegqi-inv-auto-unfold"); + Trace("cegqi-inv-auto-unfold") + << "...status = " << status << std::endl; } - - if (tmode != SYGUS_INV_TEMPL_MODE_NONE) + if (status == 1) { - //if we are doing invariant templates, then construct the template - Trace("cegqi-si") << "- Do transition inference..." << std::endl; - d_ti[q].process( qq ); - Trace("cegqi-inv") << std::endl; - if( !d_ti[q].d_func.isNull() ){ - // map the program back via non-single invocation map - Node prog = d_ti[q].d_func; - std::vector< Node > prog_templ_vars; - prog_templ_vars.insert( prog_templ_vars.end(), d_ti[q].d_vars.begin(), d_ti[q].d_vars.end() ); - d_trans_pre[prog] = d_ti[q].getComponent( 1 ); - d_trans_post[prog] = d_ti[q].getComponent( -1 ); - Trace("cegqi-inv") << " precondition : " << d_trans_pre[prog] << std::endl; - Trace("cegqi-inv") << " postcondition : " << d_trans_post[prog] << std::endl; - std::vector<Node> sivars; - d_sip->getSingleInvocationVariables(sivars); - Node invariant = d_sip->getFunctionInvocationFor(prog); - Assert(!invariant.isNull()); - invariant = invariant.substitute(sivars.begin(), - sivars.end(), - prog_templ_vars.begin(), - prog_templ_vars.end()); - Trace("cegqi-inv") << " invariant : " << invariant << std::endl; - - // store simplified version of quantified formula - d_simp_quant = d_sip->getFullSpecification(); - std::vector< Node > new_bv; - for (unsigned j = 0, size = sivars.size(); j < size; j++) - { - new_bv.push_back( - NodeManager::currentNM()->mkBoundVar(sivars[j].getType())); - } - d_simp_quant = d_simp_quant.substitute( - sivars.begin(), sivars.end(), new_bv.begin(), new_bv.end()); - Assert( q[1].getKind()==NOT && q[1][0].getKind()==FORALL ); - for( unsigned j=0; j<q[1][0][0].getNumChildren(); j++ ){ - new_bv.push_back( q[1][0][0][j] ); - } - d_simp_quant = NodeManager::currentNM()->mkNode( kind::FORALL, NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, new_bv ), d_simp_quant ).negate(); - d_simp_quant = Rewriter::rewrite( d_simp_quant ); - d_simp_quant = NodeManager::currentNM()->mkNode( kind::FORALL, q[0], d_simp_quant, q[2] ); - Trace("cegqi-si") << "Rewritten quantifier : " << d_simp_quant << std::endl; - - //construct template argument - d_templ_arg[prog] = NodeManager::currentNM()->mkSkolem( "I", invariant.getType() ); - - //construct template - Node templ; - if( options::sygusInvAutoUnfold() ){ - if( d_ti[q].isComplete() ){ - Trace("cegqi-inv-auto-unfold") << "Automatic deterministic unfolding... " << std::endl; - // auto-unfold - DetTrace dt; - int init_dt = d_ti[q].initializeTrace( dt ); - if( init_dt==0 ){ - Trace("cegqi-inv-auto-unfold") << " Init : "; - dt.print("cegqi-inv-auto-unfold"); - Trace("cegqi-inv-auto-unfold") << std::endl; - unsigned counter = 0; - unsigned status = 0; - while( counter<100 && status==0 ){ - status = d_ti[q].incrementTrace( dt ); - counter++; - Trace("cegqi-inv-auto-unfold") << " #" << counter << " : "; - dt.print("cegqi-inv-auto-unfold"); - Trace("cegqi-inv-auto-unfold") << "...status = " << status << std::endl; - } - if( status==1 ){ - // we have a trivial invariant - templ = d_ti[q].constructFormulaTrace( dt ); - Trace("cegqi-inv") << "By finite deterministic terminating trace, a solution invariant is : " << std::endl; - Trace("cegqi-inv") << " " << templ << std::endl; - // FIXME : this should be unnecessary - templ = NodeManager::currentNM()->mkNode( AND, templ, d_templ_arg[prog] ); - } - }else{ - Trace("cegqi-inv-auto-unfold") << "...failed initialize." << std::endl; - } - } - } - Trace("cegqi-inv") << "Make the template... " << tmode << " " - << templ << std::endl; - if( templ.isNull() ){ - if (tmode == SYGUS_INV_TEMPL_MODE_PRE) - { - //d_templ[prog] = NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( OR, d_trans_pre[prog], invariant ), d_trans_post[prog] ); - templ = NodeManager::currentNM()->mkNode( OR, d_trans_pre[prog], d_templ_arg[prog] ); - }else{ - Assert(tmode == SYGUS_INV_TEMPL_MODE_POST); - //d_templ[prog] = NodeManager::currentNM()->mkNode( OR, d_trans_pre[prog], NodeManager::currentNM()->mkNode( AND, d_trans_post[prog], invariant ) ); - templ = NodeManager::currentNM()->mkNode( AND, d_trans_post[prog], d_templ_arg[prog] ); - } - } - Trace("cegqi-inv") << " template (pre-substitution) : " << templ << std::endl; - Assert( !templ.isNull() ); - // subsitute the template arguments - Assert(prog_templ_vars.size() == prog_vars[prog].size()); - templ = templ.substitute( prog_templ_vars.begin(), prog_templ_vars.end(), prog_vars[prog].begin(), prog_vars[prog].end() ); - Trace("cegqi-inv") << " template : " << templ << std::endl; - d_templ[prog] = templ; - } + // we have a trivial invariant + templ = d_ti[q].constructFormulaTrace(dt); + Trace("cegqi-inv") << "By finite deterministic terminating trace, a " + "solution invariant is : " + << std::endl; + Trace("cegqi-inv") << " " << templ << std::endl; + // this should be unnecessary + templ = nm->mkNode(AND, templ, d_templ_arg[prog]); } - }else{ - //we are fully single invocation - d_single_invocation = true; } + else + { + Trace("cegqi-inv-auto-unfold") << "...failed initialize." << std::endl; + } + } + } + Trace("cegqi-inv") << "Make the template... " << tmode << " " << templ + << std::endl; + if (templ.isNull()) + { + if (tmode == SYGUS_INV_TEMPL_MODE_PRE) + { + templ = nm->mkNode(OR, d_trans_pre[prog], d_templ_arg[prog]); + } + else + { + Assert(tmode == SYGUS_INV_TEMPL_MODE_POST); + templ = nm->mkNode(AND, d_trans_post[prog], d_templ_arg[prog]); } } + Trace("cegqi-inv") << " template (pre-substitution) : " << templ + << std::endl; + Assert(!templ.isNull()); + // subsitute the template arguments + Assert(prog_templ_vars.size() == prog_vars[prog].size()); + templ = templ.substitute(prog_templ_vars.begin(), + prog_templ_vars.end(), + prog_vars[prog].begin(), + prog_vars[prog].end()); + Trace("cegqi-inv") << " template : " << templ << std::endl; + d_templ[prog] = templ; } void CegSingleInv::finishInit(bool syntaxRestricted) diff --git a/src/theory/quantifiers/sygus/sygus_invariance.cpp b/src/theory/quantifiers/sygus/sygus_invariance.cpp index 24b47b216..5ea01ef57 100644 --- a/src/theory/quantifiers/sygus/sygus_invariance.cpp +++ b/src/theory/quantifiers/sygus/sygus_invariance.cpp @@ -218,15 +218,22 @@ bool NegContainsSygusInvarianceTest::invariant(TermDbSygus* tds, NodeManager::currentNM()->mkNode(kind::STRING_STRCTN, out, nbvre); Trace("sygus-pbe-cterm-debug") << "Check: " << cont << std::endl; Node contr = Rewriter::rewrite(cont); - if (contr == tds->d_false) + if (!contr.isConst()) + { + if (d_isUniversal) + { + return false; + } + } + else if (contr.getConst<bool>() == d_isUniversal) { if (Trace.isOn("sygus-pbe-cterm")) { Trace("sygus-pbe-cterm") << "PBE-cterm : enumerator : do not consider "; - Trace("sygus-pbe-cterm") << nbv << " for any " - << tds->sygusToBuiltin(x) << " since " - << std::endl; + Trace("sygus-pbe-cterm") + << nbv << " for any " << tds->sygusToBuiltin(x) << " since " + << std::endl; Trace("sygus-pbe-cterm") << " PBE-cterm : for input example : "; for (unsigned j = 0, size = d_ex[ii].size(); j < size; j++) { @@ -238,13 +245,13 @@ bool NegContainsSygusInvarianceTest::invariant(TermDbSygus* tds, Trace("sygus-pbe-cterm") << " PBE-cterm : and is not in output : " << out << std::endl; } - return true; + return !d_isUniversal; } Trace("sygus-pbe-cterm-debug2") << "...check failed, rewrites to : " << contr << std::endl; } } - return false; + return d_isUniversal; } } /* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/sygus/sygus_invariance.h b/src/theory/quantifiers/sygus/sygus_invariance.h index 59761da5c..02c249411 100644 --- a/src/theory/quantifiers/sygus/sygus_invariance.h +++ b/src/theory/quantifiers/sygus/sygus_invariance.h @@ -249,7 +249,7 @@ class DivByZeroSygusInvarianceTest : public SygusInvarianceTest class NegContainsSygusInvarianceTest : public SygusInvarianceTest { public: - NegContainsSygusInvarianceTest() {} + NegContainsSygusInvarianceTest() : d_isUniversal(false) {} /** initialize this invariance test * e is the enumerator which we are reasoning about (associated with a synth @@ -266,9 +266,19 @@ class NegContainsSygusInvarianceTest : public SygusInvarianceTest std::vector<std::vector<Node> >& ex, std::vector<Node>& exo, std::vector<unsigned>& ncind); + /** set universal + * + * This updates the semantics of this check such that *all* instead of some + * examples must fail the containment test. + */ + void setUniversal() { d_isUniversal = true; } protected: - /** checks if contains( out_i, nvn[in_i] ) --> false for some I/O pair i. */ + /** + * Checks if contains( out_i, nvn[in_i] ) --> false for some I/O pair i; if + * d_isUniversal is true, then we check if the rewrite holds for *all* I/O + * pairs. + */ bool invariant(TermDbSygus* tds, Node nvn, Node x) override; private: @@ -282,6 +292,8 @@ class NegContainsSygusInvarianceTest : public SygusInvarianceTest * contains( out_i, nvn[in_i] ) ---> false */ std::vector<unsigned> d_neg_con_indices; + /** requires not being in all examples */ + bool d_isUniversal; }; } /* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index e8aa0a7f0..7891814be 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -272,6 +272,10 @@ bool SygusPbe::initialize(Node n, Assert(!ag.isNull()); disj.push_back(ag.negate()); Node lem = disj.size() == 1 ? disj[0] : nm->mkNode(OR, disj); + // Apply extended rewriting on the lemma. This helps utilities like + // SygusEnumerator more easily recognize the shape of this lemma, e.g. + // ( ~is-ite(x) or ( ~is-ite(x) ^ P ) ) --> ~is-ite(x). + lem = d_tds->getExtRewriter()->extendedRewrite(lem); Trace("sygus-pbe") << " static redundant op lemma : " << lem << std::endl; // Register as a symmetry breaking lemma with the term database. diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp index 89619639d..c9db62735 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp @@ -431,10 +431,13 @@ void SubsumeTrie::getLeavesInternal(const std::vector<Node>& vals, { if (index == vals.size()) { + // by convention, if we did not test any points, then we consider the + // evaluation along the current path to be always false. + int rstatus = status == -2 ? -1 : status; Assert(!d_term.isNull()); - Assert(std::find(v[status].begin(), v[status].end(), d_term) - == v[status].end()); - v[status].push_back(d_term); + Assert(std::find(v[rstatus].begin(), v[rstatus].end(), d_term) + == v[rstatus].end()); + v[rstatus].push_back(d_term); } else { @@ -806,9 +809,13 @@ Node SygusUnifIo::constructSolutionNode(std::vector<Node>& lemmas) || (!d_solution.isNull() && d_tds->getSygusTermSize(vcc) < d_sol_term_size))) { - Trace("sygus-pbe") << "**** SygusUnif SOLVED : " << c << " = " << vcc - << std::endl; - Trace("sygus-pbe") << "...solved at iteration " << i << std::endl; + if (Trace.isOn("sygus-pbe")) + { + Trace("sygus-pbe") << "**** SygusUnif SOLVED : " << c << " = "; + TermDbSygus::toStreamSygus("sygus-pbe", vcc); + Trace("sygus-pbe") << std::endl; + Trace("sygus-pbe") << "...solved at iteration " << i << std::endl; + } d_solution = vcc; newSolution = vcc; d_sol_term_size = d_tds->getSygusTermSize(vcc); @@ -867,12 +874,12 @@ bool SygusUnifIo::useStrContainsEnumeratorExclude(Node e) d_use_str_contains_eexc[e] = false; return false; } + d_use_str_contains_eexc_conditional[e] = false; if (eis.isConditional()) { Trace("sygus-sui-enum-debug") << " conditional slave : " << sn << std::endl; - d_use_str_contains_eexc[e] = false; - return false; + d_use_str_contains_eexc_conditional[e] = true; } } Trace("sygus-sui-enum-debug") @@ -895,6 +902,9 @@ bool SygusUnifIo::getExplanationForEnumeratorExclude( // the output for some input/output pair. If so, then this term is never // useful. We generalize its explanation below. + // if the enumerator is in a conditional context, then we are stricter + // about when to exclude + bool isConditional = d_use_str_contains_eexc_conditional[e]; if (Trace.isOn("sygus-sui-cterm-debug")) { Trace("sygus-sui-enum") << std::endl; @@ -921,12 +931,20 @@ bool SygusUnifIo::getExplanationForEnumeratorExclude( else { Trace("sygus-sui-cterm-debug") << "...contained." << std::endl; + if (isConditional) + { + return false; + } } } if (!cmp_indices.empty()) { // we check invariance with respect to a negative contains test NegContainsSygusInvarianceTest ncset; + if (isConditional) + { + ncset.setUniversal(); + } ncset.init(e, d_examples, d_examples_out, cmp_indices); // construct the generalized explanation d_tds->getExplain()->getExplanationFor(e, v, exp, ncset); @@ -992,10 +1010,13 @@ Node SygusUnifIo::constructSol( EnumCache& ecache = d_ecache[e]; + bool retValMod = x.isReturnValueModified(); + Node ret_dt; + Node cached_ret_dt; if (nrole == role_equal) { - if (!x.isReturnValueModified()) + if (!retValMod) { if (ecache.isSolved()) { @@ -1069,11 +1090,86 @@ Node SygusUnifIo::constructSol( } } } + // maybe we can find one in the cache + if (ret_dt.isNull() && !retValMod) + { + bool firstTime = true; + std::unordered_set<Node, NodeHashFunction> intersection; + std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>::iterator + pit; + for (size_t i = 0, nvals = x.d_vals.size(); i < nvals; i++) + { + if (x.d_vals[i].getConst<bool>()) + { + pit = d_psolutions[i].find(etn); + if (pit == d_psolutions[i].end()) + { + // no cached solution + intersection.clear(); + break; + } + if (firstTime) + { + intersection = pit->second; + firstTime = false; + } + else + { + std::vector<Node> rm; + for (const Node& a : intersection) + { + if (pit->second.find(a) == pit->second.end()) + { + rm.push_back(a); + } + } + for (const Node& a : rm) + { + intersection.erase(a); + } + if (intersection.empty()) + { + break; + } + } + } + } + if (!intersection.empty()) + { + if (d_enableMinimality) + { + // if we are enabling minimality, the minimal cached solution may + // still not be the best solution, thus we remember it and keep it if + // we don't construct a better one below + std::vector<Node> intervec; + intervec.insert( + intervec.begin(), intersection.begin(), intersection.end()); + cached_ret_dt = getMinimalTerm(intervec); + } + else + { + ret_dt = *intersection.begin(); + } + if (Trace.isOn("sygus-sui-dt")) + { + indent("sygus-sui-dt", ind); + Trace("sygus-sui-dt") << "ConstructPBE: found in cache: "; + Node csol = ret_dt; + if (d_enableMinimality) + { + csol = cached_ret_dt; + Trace("sygus-sui-dt") << "(minimal) "; + } + TermDbSygus::toStreamSygus("sygus-sui-dt", csol); + Trace("sygus-sui-dt") << std::endl; + } + } + } } else if (nrole == role_string_prefix || nrole == role_string_suffix) { // check if each return value is a prefix/suffix of all open examples - if (!x.isReturnValueModified() || x.getCurrentRole() == nrole) + if (!retValMod || x.getCurrentRole() == nrole) { std::map<Node, std::vector<unsigned> > incr; bool isPrefix = nrole == role_string_prefix; @@ -1227,7 +1323,6 @@ Node SygusUnifIo::constructSol( Trace("sygus-sui-dt") << "...try STRATEGY " << strat << "..." << std::endl; - std::map<unsigned, Node> look_ahead_solved_children; std::vector<Node> dt_children_cons; bool success = true; @@ -1242,109 +1337,95 @@ Node SygusUnifIo::constructSol( Trace("sygus-sui-dt") << "construct PBE child #" << sc << "..." << std::endl; Node rec_c; - std::map<unsigned, Node>::iterator itla = - look_ahead_solved_children.find(sc); - if (itla != look_ahead_solved_children.end()) + + std::pair<Node, NodeRole>& cenum = etis->d_cenum[sc]; + + // update the context + std::vector<Node> prev; + if (strat == strat_ITE && sc > 0) { - rec_c = itla->second; - indent("sygus-sui-dt-debug", ind + 1); - Trace("sygus-sui-dt-debug") - << "ConstructPBE: look ahead solved : " - << d_tds->sygusToBuiltin(rec_c) << std::endl; + EnumCache& ecache_cond = d_ecache[split_cond_enum]; + Assert(set_split_cond_res_index); + Assert(split_cond_res_index < ecache_cond.d_enum_vals_res.size()); + prev = x.d_vals; + x.updateContext(this, + ecache_cond.d_enum_vals_res[split_cond_res_index], + sc == 1); + // return value of above call may be false in corner cases where we + // must choose a non-separating condition to traverse to another + // strategy node } - else - { - std::pair<Node, NodeRole>& cenum = etis->d_cenum[sc]; - - // update the context - std::vector<Node> prev; - if (strat == strat_ITE && sc > 0) - { - EnumCache& ecache_cond = d_ecache[split_cond_enum]; - Assert(set_split_cond_res_index); - Assert(split_cond_res_index < ecache_cond.d_enum_vals_res.size()); - prev = x.d_vals; - bool ret = x.updateContext( - this, - ecache_cond.d_enum_vals_res[split_cond_res_index], - sc == 1); - AlwaysAssert(ret); - } - // recurse - if (strat == strat_ITE && sc == 0) - { - Node ce = cenum.first; + // recurse + if (strat == strat_ITE && sc == 0) + { + Node ce = cenum.first; - EnumCache& ecache_child = d_ecache[ce]; + EnumCache& ecache_child = d_ecache[ce]; - // get the conditionals in the current context : they must be - // distinguishable - std::map<int, std::vector<Node> > possible_cond; - std::map<Node, int> solved_cond; // stores branch - ecache_child.d_term_trie.getLeaves(x.d_vals, true, possible_cond); + // get the conditionals in the current context : they must be + // distinguishable + std::map<int, std::vector<Node> > possible_cond; + std::map<Node, int> solved_cond; // stores branch + ecache_child.d_term_trie.getLeaves(x.d_vals, true, possible_cond); - std::map<int, std::vector<Node> >::iterator itpc = - possible_cond.find(0); - if (itpc != possible_cond.end()) + std::map<int, std::vector<Node>>::iterator itpc = + possible_cond.find(0); + if (itpc != possible_cond.end()) + { + if (Trace.isOn("sygus-sui-dt-debug")) { - if (Trace.isOn("sygus-sui-dt-debug")) + indent("sygus-sui-dt-debug", ind + 1); + Trace("sygus-sui-dt-debug") + << "PBE : We have " << itpc->second.size() + << " distinguishable conditionals:" << std::endl; + for (Node& cond : itpc->second) { - indent("sygus-sui-dt-debug", ind + 1); + indent("sygus-sui-dt-debug", ind + 2); Trace("sygus-sui-dt-debug") - << "PBE : We have " << itpc->second.size() - << " distinguishable conditionals:" << std::endl; - for (Node& cond : itpc->second) - { - indent("sygus-sui-dt-debug", ind + 2); - Trace("sygus-sui-dt-debug") - << d_tds->sygusToBuiltin(cond) << std::endl; - } - } - - // otherwise, guess a conditional - if (rec_c.isNull()) - { - rec_c = constructBestConditional(ce, itpc->second); - Assert(!rec_c.isNull()); - indent("sygus-sui-dt", ind); - Trace("sygus-sui-dt") - << "PBE: ITE strategy : choose best conditional " - << d_tds->sygusToBuiltin(rec_c) << std::endl; + << d_tds->sygusToBuiltin(cond) << std::endl; } } - else + if (rec_c.isNull()) { - // TODO (#1250) : degenerate case where children have different - // types? + rec_c = constructBestConditional(ce, itpc->second); + Assert(!rec_c.isNull()); indent("sygus-sui-dt", ind); - Trace("sygus-sui-dt") << "return PBE: failed ITE strategy, " - "cannot find a distinguishable condition" - << std::endl; - } - if (!rec_c.isNull()) - { - Assert(ecache_child.d_enum_val_to_index.find(rec_c) - != ecache_child.d_enum_val_to_index.end()); - split_cond_res_index = ecache_child.d_enum_val_to_index[rec_c]; - set_split_cond_res_index = true; - split_cond_enum = ce; - Assert(split_cond_res_index - < ecache_child.d_enum_vals_res.size()); + Trace("sygus-sui-dt") + << "PBE: ITE strategy : choose best conditional " + << d_tds->sygusToBuiltin(rec_c) << std::endl; } } else { - did_recurse = true; - rec_c = constructSol(f, cenum.first, cenum.second, ind + 2, lemmas); + // TODO (#1250) : degenerate case where children have different + // types? + indent("sygus-sui-dt", ind); + Trace("sygus-sui-dt") << "return PBE: failed ITE strategy, " + "cannot find a distinguishable condition" + << std::endl; } - - // undo update the context - if (strat == strat_ITE && sc > 0) + if (!rec_c.isNull()) { - x.d_vals = prev; + Assert(ecache_child.d_enum_val_to_index.find(rec_c) + != ecache_child.d_enum_val_to_index.end()); + split_cond_res_index = ecache_child.d_enum_val_to_index[rec_c]; + set_split_cond_res_index = true; + split_cond_enum = ce; + Assert(split_cond_res_index + < ecache_child.d_enum_vals_res.size()); } } + else + { + did_recurse = true; + rec_c = constructSol(f, cenum.first, cenum.second, ind + 2, lemmas); + } + // undo update the context + if (strat == strat_ITE && sc > 0) + { + x.d_vals = prev; + } if (!rec_c.isNull()) { dt_children_cons.push_back(rec_c); @@ -1380,9 +1461,54 @@ Node SygusUnifIo::constructSol( sindex++; } + // if there was a cached solution, process it now + if (!cached_ret_dt.isNull() && cached_ret_dt != ret_dt) + { + if (ret_dt.isNull()) + { + // take the cached one if it is the only one + ret_dt = cached_ret_dt; + } + else if (d_enableMinimality) + { + Assert(ret_dt.getType() == cached_ret_dt.getType()); + // take the cached one if it is smaller + std::vector<Node> retDts; + retDts.push_back(cached_ret_dt); + retDts.push_back(ret_dt); + ret_dt = getMinimalTerm(retDts); + } + } Assert(ret_dt.isNull() || ret_dt.getType() == e.getType()); - indent("sygus-sui-dt", ind); - Trace("sygus-sui-dt") << "ConstructPBE: returned " << ret_dt << std::endl; + if (Trace.isOn("sygus-sui-dt")) + { + indent("sygus-sui-dt", ind); + Trace("sygus-sui-dt") << "ConstructPBE: returned "; + TermDbSygus::toStreamSygus("sygus-sui-dt", ret_dt); + Trace("sygus-sui-dt") << std::endl; + } + // remember the solution + if (nrole == role_equal) + { + if (!retValMod && !ret_dt.isNull()) + { + for (size_t i = 0, nvals = x.d_vals.size(); i < nvals; i++) + { + if (x.d_vals[i].getConst<bool>()) + { + if (Trace.isOn("sygus-sui-cache")) + { + indent("sygus-sui-cache", ind); + Trace("sygus-sui-cache") << "Cache solution (#" << i << ") : "; + TermDbSygus::toStreamSygus("sygus-sui-cache", ret_dt); + Trace("sygus-sui-cache") << std::endl; + } + d_psolutions[i][etn].insert(ret_dt); + } + } + } + } + return ret_dt; } diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.h b/src/theory/quantifiers/sygus/sygus_unif_io.h index 2f87c0552..7f48645bf 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.h +++ b/src/theory/quantifiers/sygus/sygus_unif_io.h @@ -183,12 +183,14 @@ class SubsumeTrie bool pol, std::vector<Node>& subsumed_by); /** - * Get the leaves of the trie, which we store in the map v. - * v[-1] stores the children that always evaluate to !pol, - * v[1] stores the children that always evaluate to pol, - * v[0] stores the children that both evaluate to true and false for at least - * one example. - */ + * Get the leaves of the trie, which we store in the map v. We consider their + * evaluation on points such that (pol ? vals : !vals) is true. + * + * v[-1] stores the children that always evaluate to !pol, + * v[1] stores the children that always evaluate to pol, + * v[0] stores the children that both evaluate to true and false for at least + * one example. + */ void getLeaves(const std::vector<Node>& vals, bool pol, std::map<int, std::vector<Node>>& v); @@ -300,6 +302,16 @@ class SygusUnifIo : public SygusUnif Node d_solution; /** the term size of the above solution */ unsigned d_sol_term_size; + /** partial solutions + * + * Maps indices for I/O points to a list of solutions for that point, for each + * type. We may have more than one type for solutions, e.g. for grammar: + * A -> ite( A, B, C ) | ... + * where terms of type B and C can both act as solutions. + */ + std::map<size_t, + std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>> + d_psolutions; /** * This flag is set to true if the solution construction was * non-deterministic with respect to failure/success. @@ -427,6 +439,12 @@ class SygusUnifIo : public SygusUnif bool useStrContainsEnumeratorExclude(Node e); /** cache for the above function */ std::map<Node, bool> d_use_str_contains_eexc; + /** + * cache for the above function, stores whether enumerators e are in + * a conditional context, e.g. used for enumerating the return values for + * leaves of ITE trees. + */ + std::map<Node, bool> d_use_str_contains_eexc_conditional; /** the unification context used within constructSolution */ UnifContextIo d_context; diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index f8e8ed5ad..4c9cf2c8d 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -654,7 +654,15 @@ bool TermUtil::isNegate(Kind k) return k == NOT || k == BITVECTOR_NOT || k == BITVECTOR_NEG || k == UMINUS; } -bool TermUtil::isAssoc( Kind k ) { +bool TermUtil::isAssoc(Kind k, bool reqNAry) +{ + if (reqNAry) + { + if (k == UNION || k == INTERSECTION) + { + return false; + } + } return k == PLUS || k == MULT || k == NONLINEAR_MULT || k == AND || k == OR || k == XOR || k == BITVECTOR_PLUS || k == BITVECTOR_MULT || k == BITVECTOR_AND || k == BITVECTOR_OR || k == BITVECTOR_XOR @@ -663,7 +671,15 @@ bool TermUtil::isAssoc( Kind k ) { || k == SEP_STAR; } -bool TermUtil::isComm( Kind k ) { +bool TermUtil::isComm(Kind k, bool reqNAry) +{ + if (reqNAry) + { + if (k == UNION || k == INTERSECTION) + { + return false; + } + } return k == EQUAL || k == PLUS || k == MULT || k == NONLINEAR_MULT || k == AND || k == OR || k == XOR || k == BITVECTOR_PLUS || k == BITVECTOR_MULT || k == BITVECTOR_AND || k == BITVECTOR_OR || k == BITVECTOR_XOR diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h index dd3e76ee2..820821991 100644 --- a/src/theory/quantifiers/term_util.h +++ b/src/theory/quantifiers/term_util.h @@ -270,10 +270,18 @@ public: * double negation if applicable, e.g. mkNegate( ~, ~x ) ---> x. */ static Node mkNegate(Kind notk, Node n); - /** is assoc */ - static bool isAssoc( Kind k ); - /** is k commutative? */ - static bool isComm( Kind k ); + /** is k associative? + * + * If flag reqNAry is true, then we additionally require that k is an + * n-ary operator. + */ + static bool isAssoc(Kind k, bool reqNAry = false); + /** is k commutative? + * + * If flag reqNAry is true, then we additionally require that k is an + * n-ary operator. + */ + static bool isComm(Kind k, bool reqNAry = false); /** is k non-additive? * Returns true if diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 320f50afb..433621d31 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -30,7 +30,6 @@ #include "theory/quantifiers/equality_infer.h" #include "theory/quantifiers/equality_query.h" #include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/fmf/ambqi_builder.h" #include "theory/quantifiers/fmf/bounded_integers.h" #include "theory/quantifiers/fmf/full_model_check.h" #include "theory/quantifiers/fmf/model_engine.h" @@ -249,20 +248,14 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, d_model.reset(new quantifiers::fmcheck::FirstOrderModelFmc( this, c, "FirstOrderModelFmc")); d_builder.reset(new quantifiers::fmcheck::FullModelChecker(c, this)); - }else if( options::mbqiMode()==quantifiers::MBQI_ABS ){ - Trace("quant-engine-debug") << "...make abs mbqi builder." << std::endl; - d_model.reset( - new quantifiers::FirstOrderModelAbs(this, c, "FirstOrderModelAbs")); - d_builder.reset(new quantifiers::AbsMbqiBuilder(c, this)); }else{ Trace("quant-engine-debug") << "...make default model builder." << std::endl; d_model.reset( - new quantifiers::FirstOrderModelIG(this, c, "FirstOrderModelIG")); - d_builder.reset(new quantifiers::QModelBuilderDefault(c, this)); + new quantifiers::FirstOrderModel(this, c, "FirstOrderModel")); + d_builder.reset(new quantifiers::QModelBuilder(c, this)); } }else{ - d_model.reset( - new quantifiers::FirstOrderModelIG(this, c, "FirstOrderModelIG")); + d_model.reset(new quantifiers::FirstOrderModel(this, c, "FirstOrderModel")); } } diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 83c66c2d3..1c302573e 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -1543,6 +1543,12 @@ void TheorySetsPrivate::checkMinCard( std::vector< Node >& lemmas ) { for( int i=(int)(d_set_eqc.size()-1); i>=0; i-- ){ Node eqc = d_set_eqc[i]; + TypeNode tn = eqc.getType().getSetElementType(); + if (d_t_card_enabled.find(tn) == d_t_card_enabled.end()) + { + // cardinality is not enabled for this type, skip + continue; + } //get members in class std::map< Node, std::map< Node, Node > >::iterator itm = d_pol_mems[0].find( eqc ); if( itm!=d_pol_mems[0].end() ){ diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index a3f1f9893..2a2015319 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -47,7 +47,7 @@ bool checkConstantMembership(TNode elementTerm, TNode setTerm) RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { NodeManager* nm = NodeManager::currentNM(); Kind kind = node.getKind(); - + Trace("sets-postrewrite") << "Process: " << node << std::endl; if(node.isConst()) { // Dare you touch the const and mangle it to something else. @@ -204,6 +204,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { if( rew!=node ){ Trace("sets-rewrite") << "Sets::rewrite " << node << " -> " << rew << std::endl; } + Trace("sets-rewrite") << "...no rewrite." << std::endl; return RewriteResponse(REWRITE_DONE, rew); } break; diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 6d0c6264b..b8e960f7b 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -1663,9 +1663,9 @@ void TheoryStrings::checkExtfEval( int effort ) { << ", const = " << einfo.d_const << std::endl; for (const Node& nrcc : nrc) { - sendInference(einfo.d_exp, - einfo.d_const == d_false ? nrcc.negate() : nrcc, - effort == 0 ? "EXTF_d" : "EXTF_d-N"); + sendInternalInference(einfo.d_exp, + einfo.d_const == d_false ? nrcc.negate() : nrcc, + effort == 0 ? "EXTF_d" : "EXTF_d-N"); } }else{ to_reduce = nrc; diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp index a3e058569..42847dfd4 100644 --- a/src/theory/uf/theory_uf_model.cpp +++ b/src/theory/uf/theory_uf_model.cpp @@ -37,17 +37,6 @@ void UfModelTreeNode::clear(){ d_value = Node::null(); } -bool UfModelTreeNode::hasConcreteArgumentDefinition(){ - if( d_data.size()>1 ){ - return true; - }else if( d_data.empty() ){ - return false; - }else{ - Node r; - return d_data.find( r )==d_data.end(); - } -} - //set value function void UfModelTreeNode::setValue( TheoryModel* m, Node n, Node v, std::vector< int >& indexOrder, bool ground, int argIndex ){ if( d_data.empty() ){ @@ -67,75 +56,6 @@ void UfModelTreeNode::setValue( TheoryModel* m, Node n, Node v, std::vector< int } } -//get value function -Node UfModelTreeNode::getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int& depIndex, int argIndex ){ - if( !d_value.isNull() && isTotal( n.getOperator(), argIndex ) ){ - //Notice() << "Constant, return " << d_value << ", depIndex = " << argIndex << std::endl; - depIndex = argIndex; - return d_value; - }else{ - Node val; - int childDepIndex[2] = { argIndex, argIndex }; - for( int i=0; i<2; i++ ){ - //first check the argument, then check default - Node r; - if( i==0 ){ - r = m->getRepresentative( n[ indexOrder[argIndex] ] ); - } - std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r ); - if( it!=d_data.end() ){ - val = it->second.getValue( m, n, indexOrder, childDepIndex[i], argIndex+1 ); - if( !val.isNull() ){ - break; - } - }else{ - //argument is not a defined argument: thus, it depends on this argument - childDepIndex[i] = argIndex+1; - } - } - //update depIndex - depIndex = childDepIndex[0]>childDepIndex[1] ? childDepIndex[0] : childDepIndex[1]; - //Notice() << "Return " << val << ", depIndex = " << depIndex; - //Notice() << " ( " << childDepIndex[0] << ", " << childDepIndex[1] << " )" << std::endl; - return val; - } -} - -Node UfModelTreeNode::getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, std::vector< int >& depIndex, int argIndex ){ - if( argIndex==(int)indexOrder.size() ){ - return d_value; - }else{ - Node val; - bool depArg = false; - //will try concrete value first, then default - for( int i=0; i<2; i++ ){ - Node r; - if( i==0 ){ - r = m->getRepresentative( n[ indexOrder[argIndex] ] ); - } - std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r ); - if( it!=d_data.end() ){ - val = it->second.getValue( m, n, indexOrder, depIndex, argIndex+1 ); - //we have found a value - if( !val.isNull() ){ - if( i==0 ){ - depArg = true; - } - break; - } - } - } - //it depends on this argument if we found it via concrete argument value, - // or if found by default/disequal from some concrete argument value(s). - if( depArg || hasConcreteArgumentDefinition() ){ - if( std::find( depIndex.begin(), depIndex.end(), indexOrder[argIndex] )==depIndex.end() ){ - depIndex.push_back( indexOrder[argIndex] ); - } - } - return val; - } -} - Node UfModelTreeNode::getFunctionValue(std::vector<Node>& args, int index, Node argDefaultValue, bool simplify) { if(!d_data.empty()) { Node defaultValue = argDefaultValue; @@ -264,10 +184,6 @@ bool UfModelTreeNode::isTotal( Node op, int argIndex ){ } } -Node UfModelTreeNode::getConstantValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int argIndex ){ - return d_value; -} - void indent( std::ostream& out, int ind ){ for( int i=0; i<ind; i++ ){ out << " "; diff --git a/src/theory/uf/theory_uf_model.h b/src/theory/uf/theory_uf_model.h index 201faccee..ac57bde27 100644 --- a/src/theory/uf/theory_uf_model.h +++ b/src/theory/uf/theory_uf_model.h @@ -31,8 +31,6 @@ public: std::map< Node, UfModelTreeNode > d_data; /** the value of this tree node (if all paths lead to same value) */ Node d_value; - /** has concrete argument defintion */ - bool hasConcreteArgumentDefinition(); public: //is this model tree empty? bool isEmpty() { return d_data.empty() && d_value.isNull(); } @@ -40,11 +38,6 @@ public: void clear(); /** setValue function */ void setValue( TheoryModel* m, Node n, Node v, std::vector< int >& indexOrder, bool ground, int argIndex ); - /** getValue function */ - Node getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int& depIndex, int argIndex ); - Node getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, std::vector< int >& depIndex, int argIndex ); - /** getConstant Value function */ - Node getConstantValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int argIndex ); /** getFunctionValue */ Node getFunctionValue( std::vector< Node >& args, int index, Node argDefaultValue, bool simplify = true ); /** update function */ @@ -92,36 +85,6 @@ public: void setDefaultValue( TheoryModel* m, Node v ){ d_tree.setValue( m, Node::null(), v, d_index_order, false, 0 ); } - /** getValue function - * - * returns val, the value of ground term n - * Say n is f( t_0...t_n ) - * depIndex is the index for which every term of the form f( t_0 ... t_depIndex, *,... * ) is equal to val - * for example, if g( x_0, x_1, x_2 ) := lambda x_0 x_1 x_2. if( x_1==a ) b else c, - * then g( a, a, a ) would return b with depIndex = 1 - * - */ - Node getValue( TheoryModel* m, Node n, int& depIndex ){ - return d_tree.getValue( m, n, d_index_order, depIndex, 0 ); - } - /** -> implementation incomplete */ - Node getValue( TheoryModel* m, Node n, std::vector< int >& depIndex ){ - return d_tree.getValue( m, n, d_index_order, depIndex, 0 ); - } - /** getConstantValue function - * - * given term n, where n may contain "all value" arguments, aka model basis arguments - * if n is null, then every argument of n is considered "all value" - * if n is constant for the entire domain specified by n, then this function returns the value of its domain - * otherwise, it returns null - * for example, say the term e represents "all values" - * if f( x_0, x_1 ) := if( x_0 = a ) b else if( x_1 = a ) a else b, - * then f( a, e ) would return b, while f( e, a ) would return null - * -> implementation incomplete - */ - Node getConstantValue( TheoryModel* m, Node n ) { - return d_tree.getConstantValue( m, n, d_index_order, 0 ); - } /** getFunctionValue * Returns a representation of this function. */ @@ -136,8 +99,6 @@ public: void simplify() { d_tree.simplify( d_op, Node::null(), 0 ); } /** is this tree total? */ bool isTotal() { return d_tree.isTotal( d_op, 0 ); } - /** is this function constant? */ - bool isConstant( TheoryModel* m ) { return !getConstantValue( m, Node::null() ).isNull(); } /** is this tree empty? */ bool isEmpty() { return d_tree.isEmpty(); } public: diff --git a/src/util/sexpr.h b/src/util/sexpr.h index 427eba5f8..bad6cdb2b 100644 --- a/src/util/sexpr.h +++ b/src/util/sexpr.h @@ -13,7 +13,7 @@ ** ** Simple representation of S-expressions. ** These are used when a simple, and obvious interface for basic - ** expressions is appropraite. + ** expressions is appropriate. ** ** These are quite ineffecient. ** These are totally disconnected from any ExprManager. |