From ac6150d7992b5dd1cace8d8d6e0d308e4a741c12 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 30 Nov 2020 09:41:37 -0600 Subject: (proof-new) Proofs for regular expression elimination (#5361) Adds support for proofs for regular expression elimination in TheoryStrings::ppRewrite via a coarse-grained rule RE_ELIM. This rule is updated by this PR to distinguish whether we apply aggressive elimination. Aggressive elimination is not currently supported, since it is non-deterministic due to generating fresh BOUND_VARIABLE. --- src/expr/proof_rule.h | 10 +++--- src/theory/strings/proof_checker.cpp | 17 +++++++++-- src/theory/strings/regexp_elim.cpp | 57 +++++++++++++++++++++++++++-------- src/theory/strings/regexp_elim.h | 36 +++++++++++++++++++--- src/theory/strings/theory_strings.cpp | 27 +++++++++-------- 5 files changed, 111 insertions(+), 36 deletions(-) diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index 19efe6285..58dfd973c 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -959,11 +959,13 @@ enum class PfRule : uint32_t // fixed length of component i of the regular expression concatenation R. RE_UNFOLD_NEG_CONCAT_FIXED, // ======== Regular expression elimination - // Children: (P:F) - // Arguments: none + // Children: none + // Arguments: (F, b) // --------------------- - // Conclusion: R - // where R = strings::RegExpElimination::eliminate(F). + // Conclusion: (= F strings::RegExpElimination::eliminate(F, b)) + // where b is a Boolean indicating whether we are using aggressive + // eliminations. Notice this rule concludes (= F F) if no eliminations + // are performed for F. RE_ELIM, //======================== Code points // Children: none diff --git a/src/theory/strings/proof_checker.cpp b/src/theory/strings/proof_checker.cpp index 0b6cf6652..2726097bc 100644 --- a/src/theory/strings/proof_checker.cpp +++ b/src/theory/strings/proof_checker.cpp @@ -438,9 +438,20 @@ Node StringProofRuleChecker::checkInternal(PfRule id, } else if (id == PfRule::RE_ELIM) { - Assert(children.size() == 1); - Assert(args.empty()); - return RegExpElimination::eliminate(children[0]); + Assert(children.empty()); + Assert(args.size() == 2); + bool isAgg; + if (!getBool(args[1], isAgg)) + { + return Node::null(); + } + Node ea = RegExpElimination::eliminate(args[0], isAgg); + // if we didn't eliminate, then this trivially proves the reflexive equality + if (ea.isNull()) + { + ea = args[0]; + } + return args[0].eqNode(ea); } else if (id == PfRule::STRING_CODE_INJ) { diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp index 1d0db0e4d..aaa9ffc48 100644 --- a/src/theory/strings/regexp_elim.cpp +++ b/src/theory/strings/regexp_elim.cpp @@ -20,30 +20,58 @@ #include "theory/strings/regexp_entail.h" #include "theory/strings/theory_strings_utils.h" -using namespace CVC4; using namespace CVC4::kind; -using namespace CVC4::theory; -using namespace CVC4::theory::strings; -RegExpElimination::RegExpElimination() +namespace CVC4 { +namespace theory { +namespace strings { + +RegExpElimination::RegExpElimination(bool isAgg, + ProofNodeManager* pnm, + context::Context* c) + : d_isAggressive(isAgg), + d_pnm(pnm), + d_epg(pnm == nullptr + ? nullptr + : new EagerProofGenerator(pnm, c, "RegExpElimination::epg")) { } -Node RegExpElimination::eliminate(Node atom) +Node RegExpElimination::eliminate(Node atom, bool isAgg) { Assert(atom.getKind() == STRING_IN_REGEXP); if (atom[1].getKind() == REGEXP_CONCAT) { - return eliminateConcat(atom); + return eliminateConcat(atom, isAgg); } else if (atom[1].getKind() == REGEXP_STAR) { - return eliminateStar(atom); + return eliminateStar(atom, isAgg); } return Node::null(); } -Node RegExpElimination::eliminateConcat(Node atom) +TrustNode RegExpElimination::eliminateTrusted(Node atom) +{ + Node eatom = eliminate(atom, d_isAggressive); + if (!eatom.isNull()) + { + // Currently aggressive doesnt work due to fresh bound variables + if (isProofEnabled() && !d_isAggressive) + { + Node eq = atom.eqNode(eatom); + Node aggn = NodeManager::currentNM()->mkConst(d_isAggressive); + std::shared_ptr pn = + d_pnm->mkNode(PfRule::RE_ELIM, {}, {atom, aggn}, eq); + d_epg->setProofFor(eq, pn); + return TrustNode::mkTrustRewrite(atom, eatom, d_epg.get()); + } + return TrustNode::mkTrustRewrite(atom, eatom, nullptr); + } + return TrustNode::null(); +} + +Node RegExpElimination::eliminateConcat(Node atom, bool isAgg) { NodeManager* nm = NodeManager::currentNM(); Node x = atom[0]; @@ -217,7 +245,7 @@ Node RegExpElimination::eliminateConcat(Node atom) // otherwise, we can use indexof to represent some next occurrence if (gap_exact[i + 1] && i + 1 != size) { - if (!options::regExpElimAgg()) + if (!isAgg) { canProcess = false; break; @@ -330,7 +358,7 @@ Node RegExpElimination::eliminateConcat(Node atom) } } - if (!options::regExpElimAgg()) + if (!isAgg) { return Node::null(); } @@ -455,9 +483,9 @@ Node RegExpElimination::eliminateConcat(Node atom) return Node::null(); } -Node RegExpElimination::eliminateStar(Node atom) +Node RegExpElimination::eliminateStar(Node atom, bool isAgg) { - if (!options::regExpElimAgg()) + if (!isAgg) { return Node::null(); } @@ -580,3 +608,8 @@ Node RegExpElimination::returnElim(Node atom, Node atomElim, const char* id) << "." << std::endl; return atomElim; } +bool RegExpElimination::isProofEnabled() const { return d_pnm != nullptr; } + +} // namespace strings +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/strings/regexp_elim.h b/src/theory/strings/regexp_elim.h index 0c1acd29d..9d6fecc93 100644 --- a/src/theory/strings/regexp_elim.h +++ b/src/theory/strings/regexp_elim.h @@ -18,6 +18,8 @@ #define CVC4__THEORY__STRINGS__REGEXP_ELIM_H #include "expr/node.h" +#include "theory/eager_proof_generator.h" +#include "theory/trust_node.h" namespace CVC4 { namespace theory { @@ -33,14 +35,32 @@ namespace strings { class RegExpElimination { public: - RegExpElimination(); + /** + * @param isAgg Whether aggressive eliminations are enabled + * @param pnm The proof node manager to use (for proofs) + * @param c The context to use (for proofs) + */ + RegExpElimination(bool isAgg = false, + ProofNodeManager* pnm = nullptr, + context::Context* c = nullptr); /** eliminate membership * * This method takes as input a regular expression membership atom of the * form (str.in.re x R). If this method returns a non-null node ret, then ret * is equivalent to atom. + * + * @param atom The node to eliminate + * @param isAgg Whether we apply aggressive elimination techniques + * @return The node with regular expressions eliminated, or null if atom + * was unchanged. + */ + static Node eliminate(Node atom, bool isAgg); + + /** + * Return the trust node corresponding to rewriting n based on eliminate + * above. */ - static Node eliminate(Node atom); + TrustNode eliminateTrusted(Node atom); private: /** return elimination @@ -50,9 +70,17 @@ class RegExpElimination */ static Node returnElim(Node atom, Node atomElim, const char* id); /** elimination for regular expression concatenation */ - static Node eliminateConcat(Node atom); + static Node eliminateConcat(Node atom, bool isAgg); /** elimination for regular expression star */ - static Node eliminateStar(Node atom); + static Node eliminateStar(Node atom, bool isAgg); + /** Are proofs enabled? */ + bool isProofEnabled() const; + /** Are aggressive eliminations enabled? */ + bool d_isAggressive; + /** Pointer to the proof node manager */ + ProofNodeManager* d_pnm; + /** An eager proof generator for storing proofs in eliminate trusted above */ + std::unique_ptr d_epg; }; /* class RegExpElimination */ } // namespace strings diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index a9e2c0051..d3e9e34f1 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -997,27 +997,28 @@ void TheoryStrings::checkRegisterTermsNormalForms() TrustNode TheoryStrings::ppRewrite(TNode atom) { Trace("strings-ppr") << "TheoryStrings::ppRewrite " << atom << std::endl; + TrustNode ret; Node atomRet = atom; if (options::regExpElim() && atom.getKind() == STRING_IN_REGEXP) { // aggressive elimination of regular expression membership - Node atomElim = d_regexp_elim.eliminate(atomRet); - if (!atomElim.isNull()) + ret = d_regexp_elim.eliminateTrusted(atomRet); + if (!ret.isNull()) { - Trace("strings-ppr") << " rewrote " << atom << " -> " << atomElim + Trace("strings-ppr") << " rewrote " << atom << " -> " << ret.getNode() << " via regular expression elimination." << std::endl; - atomRet = atomElim; + atomRet = ret.getNode(); } } if( !options::stringLazyPreproc() ){ //eager preprocess here std::vector< Node > new_nodes; StringsPreprocess* p = d_esolver.getPreprocess(); - Node ret = p->processAssertion(atomRet, new_nodes); - if (ret != atomRet) + Node pret = p->processAssertion(atomRet, new_nodes); + if (pret != atomRet) { - Trace("strings-ppr") << " rewrote " << atomRet << " -> " << ret + Trace("strings-ppr") << " rewrote " << atomRet << " -> " << pret << ", with " << new_nodes.size() << " lemmas." << std::endl; for (const Node& lem : new_nodes) @@ -1026,16 +1027,16 @@ TrustNode TheoryStrings::ppRewrite(TNode atom) ++(d_statistics.d_lemmasEagerPreproc); d_out->lemma(lem); } - atomRet = ret; + atomRet = pret; + // Don't support proofs yet, thus we must return nullptr. This is the + // case even if we had proven the elimination via regexp elimination + // above. + ret = TrustNode::mkTrustRewrite(atom, atomRet, nullptr); }else{ Assert(new_nodes.empty()); } } - if (atomRet != atom) - { - return TrustNode::mkTrustRewrite(atom, atomRet, nullptr); - } - return TrustNode::null(); + return ret; } /** run the given inference step */ -- cgit v1.2.3 From 9f372f084f5c558e3ff618d02abfdb384a82e066 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 30 Nov 2020 10:56:28 -0600 Subject: Remove includes for old API from internal code (#5536) The only code including the old API now are in parser/ and main/ which will require further untangling. --- src/CMakeLists.txt | 1 - src/expr/CMakeLists.txt | 1 - src/expr/array.h | 26 ----------------------- src/expr/symbol_table.h | 1 - src/expr/type.h | 3 --- src/expr/type_properties_template.h | 2 +- src/smt/command.cpp | 2 +- src/smt/command.h | 2 -- src/smt/dump_manager.cpp | 1 - src/smt/listeners.cpp | 1 - src/smt/model_blocker.h | 2 +- src/smt/model_core_builder.h | 2 +- src/smt/proof_manager.h | 1 - src/smt_util/boolean_simplification.h | 1 - src/theory/arith/arith_static_learner.cpp | 1 - src/theory/datatypes/type_enumerator.h | 1 - src/theory/fp/fp_converter.h | 2 +- src/theory/quantifiers/expr_miner.h | 3 +-- src/theory/quantifiers/sygus/sygus_abduct.h | 2 +- src/theory/quantifiers/sygus/sygus_grammar_norm.h | 1 - src/theory/quantifiers/sygus/sygus_interpol.h | 2 +- src/theory/quantifiers/sygus/sygus_qe_preproc.h | 2 +- src/theory/smt_engine_subsolver.h | 1 - 23 files changed, 9 insertions(+), 52 deletions(-) delete mode 100644 src/expr/array.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 869699ac5..e56379f0c 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -1137,7 +1137,6 @@ install(FILES DESTINATION ${CMAKE_INSTALL_INCLUDEDIR}/cvc4) install(FILES - expr/array.h expr/array_store_all.h expr/ascription_type.h expr/emptyset.h diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index 18de83e90..391db4bd4 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -9,7 +9,6 @@ ## directory for licensing information. ## libcvc4_add_sources( - array.h array_store_all.cpp array_store_all.h ascription_type.cpp diff --git a/src/expr/array.h b/src/expr/array.h deleted file mode 100644 index 620e61ea0..000000000 --- a/src/expr/array.h +++ /dev/null @@ -1,26 +0,0 @@ -/********************* */ -/*! \file array.h - ** \verbatim - ** Top contributors (to current version): - ** Mathias Preiner, Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 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 Array types. - ** - ** Array types. - **/ - -#include "cvc4_public.h" - -#ifndef CVC4__ARRAY_H -#define CVC4__ARRAY_H - -// we get ArrayType right now by #including type.h. -// array.h is still useful for the auto-generated kinds #includes. -#include "expr/type.h" - -#endif /* CVC4__ARRAY_H */ diff --git a/src/expr/symbol_table.h b/src/expr/symbol_table.h index 35bed1dbf..d6a632ac5 100644 --- a/src/expr/symbol_table.h +++ b/src/expr/symbol_table.h @@ -24,7 +24,6 @@ #include #include "base/exception.h" -#include "expr/expr.h" #include "expr/type.h" namespace CVC4 { diff --git a/src/expr/type.h b/src/expr/type.h index 0b923f027..0c70b1667 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -35,9 +35,6 @@ struct CVC4_PUBLIC ExprManagerMapCollection; class SmtEngine; -class CVC4_PUBLIC Datatype; -class Record; - template class NodeTemplate; diff --git a/src/expr/type_properties_template.h b/src/expr/type_properties_template.h index 264d065d6..723f805b7 100644 --- a/src/expr/type_properties_template.h +++ b/src/expr/type_properties_template.h @@ -22,8 +22,8 @@ #include #include "base/check.h" -#include "expr/expr.h" #include "expr/kind.h" +#include "expr/node.h" #include "expr/type_node.h" #include "options/language.h" diff --git a/src/smt/command.cpp b/src/smt/command.cpp index e6361be9e..432910cd3 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -29,7 +29,7 @@ #include "expr/expr_iomanip.h" #include "expr/node.h" #include "expr/symbol_manager.h" -#include "expr/type.h" +#include "expr/type_node.h" #include "options/options.h" #include "options/smt_options.h" #include "printer/printer.h" diff --git a/src/smt/command.h b/src/smt/command.h index 0b86f3539..b9c1b7d73 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -29,8 +29,6 @@ #include #include "api/cvc4cpp.h" -#include "expr/expr.h" -#include "expr/type.h" #include "util/result.h" #include "util/sexpr.h" diff --git a/src/smt/dump_manager.cpp b/src/smt/dump_manager.cpp index 9d3031b4d..51fcf8b5b 100644 --- a/src/smt/dump_manager.cpp +++ b/src/smt/dump_manager.cpp @@ -14,7 +14,6 @@ #include "smt/dump_manager.h" -#include "expr/expr_manager.h" #include "options/smt_options.h" #include "smt/dump.h" #include "smt/node_command.h" diff --git a/src/smt/listeners.cpp b/src/smt/listeners.cpp index 7d34f3373..356cfa8a6 100644 --- a/src/smt/listeners.cpp +++ b/src/smt/listeners.cpp @@ -15,7 +15,6 @@ #include "smt/listeners.h" #include "expr/attribute.h" -#include "expr/expr.h" #include "expr/node_manager_attributes.h" #include "options/smt_options.h" #include "printer/printer.h" diff --git a/src/smt/model_blocker.h b/src/smt/model_blocker.h index 92d200d40..5c45a6a56 100644 --- a/src/smt/model_blocker.h +++ b/src/smt/model_blocker.h @@ -19,7 +19,7 @@ #include -#include "expr/expr.h" +#include "expr/node.h" #include "options/smt_options.h" #include "theory/theory_model.h" diff --git a/src/smt/model_core_builder.h b/src/smt/model_core_builder.h index 7a28c47f2..327933f1b 100644 --- a/src/smt/model_core_builder.h +++ b/src/smt/model_core_builder.h @@ -19,7 +19,7 @@ #include -#include "expr/expr.h" +#include "expr/node.h" #include "options/smt_options.h" #include "theory/theory_model.h" diff --git a/src/smt/proof_manager.h b/src/smt/proof_manager.h index 118b82bec..1916f0162 100644 --- a/src/smt/proof_manager.h +++ b/src/smt/proof_manager.h @@ -18,7 +18,6 @@ #define CVC4__SMT__PROOF_MANAGER_H #include "context/cdlist.h" -#include "expr/expr.h" #include "expr/node.h" #include "expr/proof_checker.h" #include "expr/proof_node.h" diff --git a/src/smt_util/boolean_simplification.h b/src/smt_util/boolean_simplification.h index 78d7f8c38..d2fbeb413 100644 --- a/src/smt_util/boolean_simplification.h +++ b/src/smt_util/boolean_simplification.h @@ -23,7 +23,6 @@ #include #include "base/check.h" -#include "expr/expr_manager_scope.h" #include "expr/node.h" namespace CVC4 { diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp index 1e031c322..f4016d032 100644 --- a/src/theory/arith/arith_static_learner.cpp +++ b/src/theory/arith/arith_static_learner.cpp @@ -18,7 +18,6 @@ #include #include "base/output.h" -#include "expr/expr.h" #include "expr/node_algorithm.h" #include "options/arith_options.h" #include "smt/smt_statistics_registry.h" diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h index a0def66c5..a090a58fe 100644 --- a/src/theory/datatypes/type_enumerator.h +++ b/src/theory/datatypes/type_enumerator.h @@ -21,7 +21,6 @@ #include "expr/dtype.h" #include "expr/kind.h" -#include "expr/type.h" #include "expr/type_node.h" #include "options/quantifiers_options.h" #include "theory/type_enumerator.h" diff --git a/src/theory/fp/fp_converter.h b/src/theory/fp/fp_converter.h index 59e65c9e1..e48d651bd 100644 --- a/src/theory/fp/fp_converter.h +++ b/src/theory/fp/fp_converter.h @@ -26,7 +26,7 @@ #include "context/cdlist.h" #include "expr/node.h" #include "expr/node_builder.h" -#include "expr/type.h" +#include "expr/type_node.h" #include "theory/valuation.h" #include "util/bitvector.h" #include "util/floatingpoint_size.h" diff --git a/src/theory/quantifiers/expr_miner.h b/src/theory/quantifiers/expr_miner.h index aa0e62891..a3938412d 100644 --- a/src/theory/quantifiers/expr_miner.h +++ b/src/theory/quantifiers/expr_miner.h @@ -21,8 +21,7 @@ #include #include -#include "expr/expr.h" -#include "expr/expr_manager.h" +#include "expr/node.h" #include "smt/smt_engine.h" #include "theory/quantifiers/sygus_sampler.h" diff --git a/src/theory/quantifiers/sygus/sygus_abduct.h b/src/theory/quantifiers/sygus/sygus_abduct.h index 9fc8e703c..d39d2a377 100644 --- a/src/theory/quantifiers/sygus/sygus_abduct.h +++ b/src/theory/quantifiers/sygus/sygus_abduct.h @@ -19,7 +19,7 @@ #include #include #include "expr/node.h" -#include "expr/type.h" +#include "expr/type_node.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.h b/src/theory/quantifiers/sygus/sygus_grammar_norm.h index acafeec3c..48a5dbe06 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.h @@ -24,7 +24,6 @@ #include "expr/node.h" #include "expr/sygus_datatype.h" -#include "expr/type.h" #include "expr/type_node.h" #include "theory/quantifiers/term_util.h" diff --git a/src/theory/quantifiers/sygus/sygus_interpol.h b/src/theory/quantifiers/sygus/sygus_interpol.h index 916f2d9b5..4db5f261a 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.h +++ b/src/theory/quantifiers/sygus/sygus_interpol.h @@ -20,7 +20,7 @@ #include #include "expr/node.h" -#include "expr/type.h" +#include "expr/type_node.h" #include "smt/smt_engine.h" namespace CVC4 { diff --git a/src/theory/quantifiers/sygus/sygus_qe_preproc.h b/src/theory/quantifiers/sygus/sygus_qe_preproc.h index 2214d4beb..daee1762f 100644 --- a/src/theory/quantifiers/sygus/sygus_qe_preproc.h +++ b/src/theory/quantifiers/sygus/sygus_qe_preproc.h @@ -18,7 +18,7 @@ #include #include #include "expr/node.h" -#include "expr/type.h" +#include "expr/type_node.h" namespace CVC4 { namespace theory { diff --git a/src/theory/smt_engine_subsolver.h b/src/theory/smt_engine_subsolver.h index f68900ccc..e2742c812 100644 --- a/src/theory/smt_engine_subsolver.h +++ b/src/theory/smt_engine_subsolver.h @@ -22,7 +22,6 @@ #include #include -#include "expr/expr_manager.h" #include "expr/node.h" #include "smt/smt_engine.h" -- cgit v1.2.3 From aa7585a6083884ad76ecc83af60020403096129a Mon Sep 17 00:00:00 2001 From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> Date: Mon, 30 Nov 2020 13:32:51 -0600 Subject: Eliminate uses of SExpr from the parser. (#5496) This is a step towards migrating Commands to the API. SExpr is an internal module that's not used by the API but is used by the parser and some commands. This PR replaces SExpr with terms of kind SEXPR in the parser and strings in commands (which brings them more inline with the API). --- src/api/cvc4cpp.cpp | 25 ++++++++++---- src/main/driver_unified.cpp | 6 ++-- src/parser/cvc/Cvc.g | 45 ++++++++++++------------- src/parser/parser.h | 1 - src/parser/smt2/Smt2.g | 69 ++++++++++++++++---------------------- src/parser/smt2/smt2.cpp | 8 ----- src/parser/smt2/smt2.h | 4 --- src/parser/tptp/Tptp.g | 2 +- src/smt/command.cpp | 82 ++++++++++++++++++++++++++++----------------- src/smt/command.h | 23 +++++++++---- src/smt/smt_engine.cpp | 10 ------ 11 files changed, 140 insertions(+), 135 deletions(-) diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 5eabcfe62..748a1ce06 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -354,6 +354,7 @@ const static std::unordered_map {CVC4::Kind::DISTINCT, DISTINCT}, {CVC4::Kind::VARIABLE, CONSTANT}, {CVC4::Kind::BOUND_VARIABLE, VARIABLE}, + {CVC4::Kind::SEXPR, SEXPR}, {CVC4::Kind::LAMBDA, LAMBDA}, {CVC4::Kind::WITNESS, WITNESS}, /* Boolean --------------------------------------------------------- */ @@ -822,6 +823,14 @@ class CVC4ApiRecoverableExceptionStream << "Invalid argument '" << arg << "' for '" << #arg \ << "', expected " +#define CVC4_API_RECOVERABLE_ARG_CHECK_EXPECTED(cond, arg) \ + CVC4_PREDICT_TRUE(cond) \ + ? (void)0 \ + : OstreamVoider() \ + & CVC4ApiRecoverableExceptionStream().ostream() \ + << "Invalid argument '" << arg << "' for '" << #arg \ + << "', expected " + #define CVC4_API_ARG_SIZE_CHECK_EXPECTED(cond, arg) \ CVC4_PREDICT_TRUE(cond) \ ? (void)0 \ @@ -842,6 +851,10 @@ class CVC4ApiRecoverableExceptionStream { #define CVC4_API_SOLVER_TRY_CATCH_END \ } \ + catch (const UnrecognizedOptionException& e) \ + { \ + throw CVC4ApiRecoverableException(e.getMessage()); \ + } \ catch (const CVC4::RecoverableModalException& e) \ { \ throw CVC4ApiRecoverableException(e.getMessage()); \ @@ -5083,7 +5096,7 @@ std::vector Solver::getAssertions(void) const std::string Solver::getInfo(const std::string& flag) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; - CVC4_API_CHECK(d_smtEngine->isValidGetInfoFlag(flag)) + CVC4_API_RECOVERABLE_CHECK(d_smtEngine->isValidGetInfoFlag(flag)) << "Unrecognized flag for getInfo."; return d_smtEngine->getInfo(flag).toString(); @@ -5415,7 +5428,7 @@ void Solver::resetAssertions(void) const void Solver::setInfo(const std::string& keyword, const std::string& value) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; - CVC4_API_ARG_CHECK_EXPECTED( + CVC4_API_RECOVERABLE_ARG_CHECK_EXPECTED( keyword == "source" || keyword == "category" || keyword == "difficulty" || keyword == "filename" || keyword == "license" || keyword == "name" || keyword == "notes" || keyword == "smt-lib-version" @@ -5423,10 +5436,10 @@ void Solver::setInfo(const std::string& keyword, const std::string& value) const keyword) << "'source', 'category', 'difficulty', 'filename', 'license', 'name', " "'notes', 'smt-lib-version' or 'status'"; - CVC4_API_ARG_CHECK_EXPECTED(keyword != "smt-lib-version" || value == "2" - || value == "2.0" || value == "2.5" - || value == "2.6", - value) + CVC4_API_RECOVERABLE_ARG_CHECK_EXPECTED( + keyword != "smt-lib-version" || value == "2" || value == "2.0" + || value == "2.5" || value == "2.6", + value) << "'2.0', '2.5', '2.6'"; CVC4_API_ARG_CHECK_EXPECTED(keyword != "status" || value == "sat" || value == "unsat" || value == "unknown", diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 673c5ddd9..ab2c8a218 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -209,7 +209,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { "--tear-down-incremental doesn't work in interactive mode"); } if(!opts.wasSetByUserIncrementalSolving()) { - cmd.reset(new SetOptionCommand("incremental", SExpr(true))); + cmd.reset(new SetOptionCommand("incremental", "true")); cmd->setMuted(true); pExecutor->doCommand(cmd); } @@ -246,7 +246,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { if(!opts.getIncrementalSolving() && opts.getTearDownIncremental() > 1) { // For tear-down-incremental values greater than 1, need incremental // on too. - cmd.reset(new SetOptionCommand("incremental", SExpr(true))); + cmd.reset(new SetOptionCommand("incremental", "true")); cmd->setMuted(true); pExecutor->doCommand(cmd); // if(opts.wasSetByUserIncrementalSolving()) { @@ -410,7 +410,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { } } else { if(!opts.wasSetByUserIncrementalSolving()) { - cmd.reset(new SetOptionCommand("incremental", SExpr(false))); + cmd.reset(new SetOptionCommand("incremental", "false")); cmd->setMuted(true); pExecutor->doCommand(cmd); } diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 91c7d0ded..30edf86cd 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -686,7 +686,7 @@ options { backtrack = true; } mainCommand[std::unique_ptr* cmd] @init { api::Term f; - SExpr sexpr; + api::Term sexpr; std::string id; api::Sort t; std::vector dts; @@ -715,14 +715,14 @@ mainCommand[std::unique_ptr* cmd] ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } ) ( symbolicExpr[sexpr] { if(s == "logic") { - cmd->reset(new SetBenchmarkLogicCommand(sexpr.getValue())); + cmd->reset(new SetBenchmarkLogicCommand(sexprToString(sexpr))); } else { - cmd->reset(new SetOptionCommand(s, sexpr)); + cmd->reset(new SetOptionCommand(s, sexprToString(sexpr))); } } - | TRUE_TOK { cmd->reset(new SetOptionCommand(s, SExpr("true"))); } - | FALSE_TOK { cmd->reset(new SetOptionCommand(s, SExpr("false"))); } - | { cmd->reset(new SetOptionCommand(s, SExpr("true"))); } + | TRUE_TOK { cmd->reset(new SetOptionCommand(s, "true")); } + | FALSE_TOK { cmd->reset(new SetOptionCommand(s, "false")); } + | { cmd->reset(new SetOptionCommand(s, "true")); } ) /* push / pop */ @@ -832,8 +832,8 @@ mainCommand[std::unique_ptr* cmd] { UNSUPPORTED("CALL command"); } | ECHO_TOK - ( simpleSymbolicExpr[sexpr] - { cmd->reset(new EchoCommand(sexpr.getValue())); } + ( simpleSymbolicExpr[s] + { cmd->reset(new EchoCommand(s)); } | { cmd->reset(new EchoCommand()); } ) @@ -939,34 +939,31 @@ mainCommand[std::unique_ptr* cmd] | toplevelDeclaration[cmd] ; -simpleSymbolicExpr[CVC4::SExpr& sexpr] -@declarations { - std::string s; - CVC4::Rational r; -} +simpleSymbolicExpr[std::string& s] : INTEGER_LITERAL - { sexpr = SExpr(Integer(AntlrInput::tokenText($INTEGER_LITERAL))); } + { s = AntlrInput::tokenText($INTEGER_LITERAL); } | MINUS_TOK INTEGER_LITERAL - { sexpr = SExpr(-Integer(AntlrInput::tokenText($INTEGER_LITERAL))); } + { s = std::to_string(MINUS_TOK) + AntlrInput::tokenText($INTEGER_LITERAL); } | DECIMAL_LITERAL - { sexpr = SExpr(AntlrInput::tokenToRational($DECIMAL_LITERAL)); } + { s = AntlrInput::tokenText($DECIMAL_LITERAL); } | HEX_LITERAL - { sexpr = SExpr(AntlrInput::tokenText($HEX_LITERAL)); } + { s = AntlrInput::tokenText($HEX_LITERAL); } | BINARY_LITERAL - { sexpr = SExpr(AntlrInput::tokenText($BINARY_LITERAL)); } + { s = AntlrInput::tokenText($BINARY_LITERAL); } | str[s] - { sexpr = SExpr(s); } | IDENTIFIER - { sexpr = SExpr(AntlrInput::tokenText($IDENTIFIER)); } + { s = AntlrInput::tokenText($IDENTIFIER); } ; -symbolicExpr[CVC4::SExpr& sexpr] +symbolicExpr[CVC4::api::Term& sexpr] @declarations { - std::vector children; + std::string s; + std::vector children; } - : simpleSymbolicExpr[sexpr] + : simpleSymbolicExpr[s] + { sexpr = SOLVER->mkString(PARSER_STATE->processAdHocStringEsc(s)); } | LPAREN (symbolicExpr[sexpr] { children.push_back(sexpr); } )* RPAREN - { sexpr = SExpr(children); } + { sexpr = SOLVER->mkTerm(CVC4::api::SEXPR, children); } ; /** diff --git a/src/parser/parser.h b/src/parser/parser.h index 96a16b31f..686a0d147 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -803,7 +803,6 @@ public: */ api::Term mkStringConstant(const std::string& s); - private: /** ad-hoc string escaping * * Returns the (internal) vector of code points corresponding to processing diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 88035dba4..6eb3d8061 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -722,29 +722,27 @@ sygusGrammar[CVC4::api::Grammar*& ret, setInfoInternal[std::unique_ptr* cmd] @declarations { std::string name; - SExpr sexpr; + api::Term sexpr; } : KEYWORD symbolicExpr[sexpr] { name = AntlrInput::tokenText($KEYWORD); - PARSER_STATE->setInfo(name.c_str() + 1, sexpr); - cmd->reset(new SetInfoCommand(name.c_str() + 1, sexpr)); + cmd->reset(new SetInfoCommand(name.c_str() + 1, sexprToString(sexpr))); } ; setOptionInternal[std::unique_ptr* cmd] @init { std::string name; - SExpr sexpr; + api::Term sexpr; } : keyword[name] symbolicExpr[sexpr] - { PARSER_STATE->setOption(name.c_str() + 1, sexpr); - cmd->reset(new SetOptionCommand(name.c_str() + 1, sexpr)); + { cmd->reset(new SetOptionCommand(name.c_str() + 1, sexprToString(sexpr))); // Ugly that this changes the state of the parser; but // global-declarations affects parsing, so we can't hold off // on this until some SmtEngine eventually (if ever) executes it. if(name == ":global-declarations") { - SYM_MAN->setGlobalDeclarations(sexpr.getValue() == "true"); + SYM_MAN->setGlobalDeclarations(sexprToString(sexpr) == "true"); } } ; @@ -755,7 +753,7 @@ smt25Command[std::unique_ptr* cmd] std::string fname; CVC4::api::Term expr, expr2; std::vector > sortedVarNames; - SExpr sexpr; + std::string s; CVC4::api::Sort t; CVC4::api::Term func; std::vector bvs; @@ -786,8 +784,8 @@ smt25Command[std::unique_ptr* cmd] /* echo */ | ECHO_TOK - ( simpleSymbolicExpr[sexpr] - { cmd->reset(new EchoCommand(sexpr.toString())); } + ( simpleSymbolicExpr[s] + { cmd->reset(new EchoCommand(s)); } | { cmd->reset(new EchoCommand()); } ) @@ -1246,30 +1244,17 @@ datatypesDef[bool isCo, } ; -simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr] -@declarations { - CVC4::Kind k; - std::string s; - std::vector s_vec; -} +simpleSymbolicExprNoKeyword[std::string& s] : INTEGER_LITERAL - { sexpr = SExpr(Integer(AntlrInput::tokenText($INTEGER_LITERAL))); } + { s = AntlrInput::tokenText($INTEGER_LITERAL); } | DECIMAL_LITERAL - { sexpr = SExpr(AntlrInput::tokenToRational($DECIMAL_LITERAL)); } + { s = AntlrInput::tokenText($DECIMAL_LITERAL); } | HEX_LITERAL - { assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 ); - std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2); - sexpr = SExpr(Integer(hexString, 16)); - } + { s = AntlrInput::tokenText($HEX_LITERAL); } | BINARY_LITERAL - { assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 ); - std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2); - sexpr = SExpr(Integer(binString, 2)); - } + { s = AntlrInput::tokenText($BINARY_LITERAL); } | str[s,false] - { sexpr = SExpr(s); } | symbol[s,CHECK_NONE,SYM_SORT] - { sexpr = SExpr(SExpr::Keyword(s)); } | tok=(ASSERT_TOK | CHECK_SAT_TOK | CHECK_SAT_ASSUMING_TOK | DECLARE_FUN_TOK | DECLARE_SORT_TOK | DEFINE_FUN_TOK | DEFINE_FUN_REC_TOK | DEFINE_FUNS_REC_TOK @@ -1279,7 +1264,7 @@ simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr] | RESET_TOK | RESET_ASSERTIONS_TOK | SET_LOGIC_TOK | SET_INFO_TOK | GET_INFO_TOK | SET_OPTION_TOK | GET_OPTION_TOK | PUSH_TOK | POP_TOK | DECLARE_DATATYPES_TOK | GET_MODEL_TOK | ECHO_TOK | SIMPLIFY_TOK) - { sexpr = SExpr(SExpr::Keyword(AntlrInput::tokenText($tok))); } + { s = AntlrInput::tokenText($tok); } ; keyword[std::string& s] @@ -1287,20 +1272,21 @@ keyword[std::string& s] { s = AntlrInput::tokenText($KEYWORD); } ; -simpleSymbolicExpr[CVC4::SExpr& sexpr] - : simpleSymbolicExprNoKeyword[sexpr] - | KEYWORD - { sexpr = SExpr(AntlrInput::tokenText($KEYWORD)); } +simpleSymbolicExpr[std::string& s] + : simpleSymbolicExprNoKeyword[s] + | KEYWORD { s = AntlrInput::tokenText($KEYWORD); } ; -symbolicExpr[CVC4::SExpr& sexpr] +symbolicExpr[CVC4::api::Term& sexpr] @declarations { - std::vector children; + std::string s; + std::vector children; } - : simpleSymbolicExpr[sexpr] + : simpleSymbolicExpr[s] + { sexpr = SOLVER->mkString(PARSER_STATE->processAdHocStringEsc(s)); } | LPAREN_TOK ( symbolicExpr[sexpr] { children.push_back(sexpr); } )* RPAREN_TOK - { sexpr = SExpr(children); } + { sexpr = SOLVER->mkTerm(CVC4::api::SEXPR, children); } ; /** @@ -1781,13 +1767,14 @@ termAtomic[CVC4::api::Term& atomTerm] */ attribute[CVC4::api::Term& expr, CVC4::api::Term& retExpr, std::string& attr] @init { - SExpr sexpr; + api::Term sexpr; + std::string s; CVC4::api::Term patexpr; std::vector patexprs; CVC4::api::Term e2; bool hasValue = false; } - : KEYWORD ( simpleSymbolicExprNoKeyword[sexpr] { hasValue = true; } )? + : KEYWORD ( simpleSymbolicExprNoKeyword[s] { hasValue = true; } )? { attr = AntlrInput::tokenText($KEYWORD); PARSER_STATE->attributeNotSupported(attr); @@ -1824,7 +1811,7 @@ attribute[CVC4::api::Term& expr, CVC4::api::Term& retExpr, std::string& attr] | tok=( ATTRIBUTE_QUANTIFIER_ID_TOK ) symbolicExpr[sexpr] { api::Sort boolType = SOLVER->getBooleanSort(); - api::Term avar = SOLVER->mkConst(boolType, sexpr.toString()); + api::Term avar = SOLVER->mkConst(boolType, sexprToString(sexpr)); attr = std::string(":qid"); retExpr = MK_TERM(api::INST_ATTRIBUTE, avar); Command* c = new SetUserAttributeCommand("qid", avar); @@ -1835,7 +1822,7 @@ attribute[CVC4::api::Term& expr, CVC4::api::Term& retExpr, std::string& attr] { attr = std::string(":named"); // notify that expression was given a name - PARSER_STATE->notifyNamedExpression(expr, sexpr.getValue()); + PARSER_STATE->notifyNamedExpression(expr, sexprToString(sexpr)); } ; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index b9279fcb0..17f5661b4 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -750,14 +750,6 @@ bool Smt2::sygus_v2() const return getLanguage() == language::input::LANG_SYGUS_V2; } -void Smt2::setInfo(const std::string& flag, const SExpr& sexpr) { - // TODO: ??? -} - -void Smt2::setOption(const std::string& flag, const SExpr& sexpr) { - // TODO: ??? -} - void Smt2::checkThatLogicIsSet() { if (!logicIsSet()) diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index fd08ab241..654ff9fbf 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -261,10 +261,6 @@ class Smt2 : public Parser */ bool escapeDupDblQuote() const { return v2_5() || sygus(); } - void setInfo(const std::string& flag, const SExpr& sexpr); - - void setOption(const std::string& flag, const SExpr& sexpr); - void checkThatLogicIsSet(); /** diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index 447a867c8..6b66b5422 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -259,7 +259,7 @@ parseCommand returns [CVC4::Command* cmd = NULL] if(filename.substr(filename.length() - 2) == ".p") { filename = filename.substr(0, filename.length() - 2); } - seq->addCommand(new SetInfoCommand("filename", SExpr(filename))); + seq->addCommand(new SetInfoCommand("filename", filename)); if(PARSER_STATE->hasConjecture()) { seq->addCommand(new QueryCommand(SOLVER->mkFalse())); } else { diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 432910cd3..14b9ed0aa 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -45,6 +45,43 @@ using namespace std; namespace CVC4 { +std::string sexprToString(api::Term sexpr) +{ + // if sexpr is a spec constant and not a string, return the result of calling + // Term::toString + if (sexpr.getKind() == api::CONST_BOOLEAN + || sexpr.getKind() == api::CONST_FLOATINGPOINT + || sexpr.getKind() == api::CONST_RATIONAL) + { + return sexpr.toString(); + } + + // if sexpr is a constant string, return the result of calling Term::toString. + // However, strip the surrounding quotes + if (sexpr.getKind() == api::CONST_STRING) + { + return sexpr.toString().substr(1, sexpr.toString().length() - 2); + } + + // if sexpr is not a spec constant, make sure it is an array of sub-sexprs + Assert(sexpr.getKind() == api::SEXPR); + + std::stringstream ss; + auto it = sexpr.begin(); + + // recursively print the sub-sexprs + ss << '(' << sexprToString(*it); + ++it; + while (it != sexpr.end()) + { + ss << ' ' << sexprToString(*it); + ++it; + } + ss << ')'; + + return ss.str(); +} + const int CommandPrintSuccess::s_iosIndex = std::ios_base::xalloc(); const CommandSuccess* CommandSuccess::s_instance = new CommandSuccess(); const CommandInterrupted* CommandInterrupted::s_instance = @@ -137,11 +174,6 @@ std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps) Command::Command() : d_commandStatus(nullptr), d_muted(false) {} -Command::Command(const api::Solver* solver) - : d_commandStatus(nullptr), d_muted(false) -{ -} - Command::Command(const Command& cmd) { d_commandStatus = @@ -1811,7 +1843,7 @@ void BlockModelValuesCommand::invoke(api::Solver* solver, SymbolManager* sm) solver->blockModelValues(d_terms); d_commandStatus = CommandSuccess::instance(); } - catch (RecoverableModalException& e) + catch (api::CVC4ApiRecoverableException& e) { d_commandStatus = new CommandRecoverableFailure(e.what()); } @@ -2520,21 +2552,21 @@ void SetBenchmarkLogicCommand::toStream(std::ostream& out, /* class SetInfoCommand */ /* -------------------------------------------------------------------------- */ -SetInfoCommand::SetInfoCommand(std::string flag, const SExpr& sexpr) +SetInfoCommand::SetInfoCommand(std::string flag, const std::string& sexpr) : d_flag(flag), d_sexpr(sexpr) { } std::string SetInfoCommand::getFlag() const { return d_flag; } -SExpr SetInfoCommand::getSExpr() const { return d_sexpr; } +const std::string& SetInfoCommand::getSExpr() const { return d_sexpr; } void SetInfoCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { - solver->getSmtEngine()->setInfo(d_flag, d_sexpr); + solver->setInfo(d_flag, d_sexpr); d_commandStatus = CommandSuccess::instance(); } - catch (UnrecognizedOptionException&) + catch (api::CVC4ApiRecoverableException&) { // As per SMT-LIB spec, silently accept unknown set-info keys d_commandStatus = CommandSuccess::instance(); @@ -2570,23 +2602,13 @@ void GetInfoCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { - vector v; - v.push_back(SExpr(SExpr::Keyword(string(":") + d_flag))); - v.emplace_back(solver->getSmtEngine()->getInfo(d_flag)); - stringstream ss; - if (d_flag == "all-options" || d_flag == "all-statistics") - { - ss << PrettySExprs(true); - } - ss << SExpr(v); - d_result = ss.str(); + std::vector v; + v.push_back(solver->mkString(":" + d_flag)); + v.push_back(solver->mkString(solver->getInfo(d_flag))); + d_result = sexprToString(solver->mkTerm(api::SEXPR, v)); d_commandStatus = CommandSuccess::instance(); } - catch (UnrecognizedOptionException&) - { - d_commandStatus = new CommandUnsupported(); - } - catch (RecoverableModalException& e) + catch (api::CVC4ApiRecoverableException& e) { d_commandStatus = new CommandRecoverableFailure(e.what()); } @@ -2630,21 +2652,21 @@ void GetInfoCommand::toStream(std::ostream& out, /* class SetOptionCommand */ /* -------------------------------------------------------------------------- */ -SetOptionCommand::SetOptionCommand(std::string flag, const SExpr& sexpr) +SetOptionCommand::SetOptionCommand(std::string flag, const std::string& sexpr) : d_flag(flag), d_sexpr(sexpr) { } std::string SetOptionCommand::getFlag() const { return d_flag; } -SExpr SetOptionCommand::getSExpr() const { return d_sexpr; } +const std::string& SetOptionCommand::getSExpr() const { return d_sexpr; } void SetOptionCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { - solver->getSmtEngine()->setOption(d_flag, d_sexpr); + solver->setOption(d_flag, d_sexpr); d_commandStatus = CommandSuccess::instance(); } - catch (UnrecognizedOptionException&) + catch (api::CVC4ApiRecoverableException&) { d_commandStatus = new CommandUnsupported(); } @@ -2682,7 +2704,7 @@ void GetOptionCommand::invoke(api::Solver* solver, SymbolManager* sm) d_result = solver->getOption(d_flag); d_commandStatus = CommandSuccess::instance(); } - catch (UnrecognizedOptionException&) + catch (api::CVC4ApiRecoverableException&) { d_commandStatus = new CommandUnsupported(); } diff --git a/src/smt/command.h b/src/smt/command.h index b9c1b7d73..bfe5e737a 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -49,6 +49,16 @@ namespace smt { class Model; } +/** + * Convert a symbolic expression to string. This method differs from + * Term::toString in that it does not surround constant strings with double + * quote symbols. + * + * @param sexpr the symbolic expression to convert + * @return the symbolic expression as string + */ +std::string sexprToString(api::Term sexpr); + std::ostream& operator<<(std::ostream&, const Command&) CVC4_PUBLIC; std::ostream& operator<<(std::ostream&, const Command*) CVC4_PUBLIC; std::ostream& operator<<(std::ostream&, const CommandStatus&) CVC4_PUBLIC; @@ -196,7 +206,6 @@ class CVC4_PUBLIC Command typedef CommandPrintSuccess printsuccess; Command(); - Command(const api::Solver* solver); Command(const Command& cmd); virtual ~Command(); @@ -1283,13 +1292,13 @@ class CVC4_PUBLIC SetInfoCommand : public Command { protected: std::string d_flag; - SExpr d_sexpr; + std::string d_sexpr; public: - SetInfoCommand(std::string flag, const SExpr& sexpr); + SetInfoCommand(std::string flag, const std::string& sexpr); std::string getFlag() const; - SExpr getSExpr() const; + const std::string& getSExpr() const; void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; @@ -1328,13 +1337,13 @@ class CVC4_PUBLIC SetOptionCommand : public Command { protected: std::string d_flag; - SExpr d_sexpr; + std::string d_sexpr; public: - SetOptionCommand(std::string flag, const SExpr& sexpr); + SetOptionCommand(std::string flag, const std::string& sexpr); std::string getFlag() const; - SExpr getSExpr() const; + const std::string& getSExpr() const; void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 0f40db530..722f6a080 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -468,11 +468,6 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) value.getValue() == "2.6" ) { ilang = language::input::LANG_SMTLIB_V2_6; } - else - { - Warning() << "Warning: unsupported smt-lib-version: " << value << endl; - throw UnrecognizedOptionException(); - } options::inputLanguage.set(ilang); // also update the output language if (!options::outputLanguage.wasSetByUser()) @@ -497,7 +492,6 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) d_state->notifyExpectedStatus(s); return; } - throw UnrecognizedOptionException(); } bool SmtEngine::isValidGetInfoFlag(const std::string& key) const @@ -517,10 +511,6 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const SmtScope smts(this); Trace("smt") << "SMT getInfo(" << key << ")" << endl; - if (!isValidGetInfoFlag(key)) - { - throw UnrecognizedOptionException(); - } if (key == "all-statistics") { vector stats; -- cgit v1.2.3 From 1b73aefa4a33b5033390f7d6c9c96fa58cd3a298 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Mon, 30 Nov 2020 12:17:43 -0800 Subject: floatingpoint: Use unique_ptr for FloatingPointLiteral pointer. (#5503) --- src/util/floatingpoint.cpp | 28 +++++++++++++--------------- src/util/floatingpoint.h | 16 ++++++++++++---- 2 files changed, 25 insertions(+), 19 deletions(-) diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp index c5ec4d0c6..5b291f3c5 100644 --- a/src/util/floatingpoint.cpp +++ b/src/util/floatingpoint.cpp @@ -129,35 +129,35 @@ FloatingPoint::FloatingPoint(const FloatingPointSize& size, #ifdef CVC4_USE_SYMFPU if (signedBV) { - d_fpl = new FloatingPointLiteral( + d_fpl.reset(new FloatingPointLiteral( symfpu::convertSBVToFloat( symfpuLiteral::CVC4FPSize(size), symfpuLiteral::CVC4RM(rm), - symfpuLiteral::CVC4SignedBitVector(bv))); + symfpuLiteral::CVC4SignedBitVector(bv)))); } else { - d_fpl = new FloatingPointLiteral( + d_fpl.reset(new FloatingPointLiteral( symfpu::convertUBVToFloat( symfpuLiteral::CVC4FPSize(size), symfpuLiteral::CVC4RM(rm), - symfpuLiteral::CVC4UnsignedBitVector(bv))); + symfpuLiteral::CVC4UnsignedBitVector(bv)))); } #else - d_fpl = new FloatingPointLiteral(2, 2, 0.0); + d_fpl.reset(new FloatingPointLiteral(2, 2, 0.0)); #endif } FloatingPoint::FloatingPoint(const FloatingPointSize& fp_size, - const FloatingPointLiteral* fpl) + FloatingPointLiteral* fpl) : d_fp_size(fp_size) { - d_fpl = new FloatingPointLiteral(*fpl); + d_fpl.reset(fpl); } FloatingPoint::FloatingPoint(const FloatingPoint& fp) : d_fp_size(fp.d_fp_size) { - d_fpl = new FloatingPointLiteral(*fp.d_fpl); + d_fpl.reset(new FloatingPointLiteral(*fp.d_fpl)); } FloatingPoint::FloatingPoint(const FloatingPointSize& size, @@ -171,10 +171,10 @@ FloatingPoint::FloatingPoint(const FloatingPointSize& size, { #ifdef CVC4_USE_SYMFPU // In keeping with the SMT-LIB standard - d_fpl = new FloatingPointLiteral( - SymFPUUnpackedFloatLiteral::makeZero(size, false)); + d_fpl.reset(new FloatingPointLiteral( + SymFPUUnpackedFloatLiteral::makeZero(size, false))); #else - d_fpl = new FloatingPointLiteral(2, 2, 0.0); + d_fpl.reset(new FloatingPointLiteral(2, 2, 0.0)); #endif } else @@ -285,8 +285,8 @@ FloatingPoint::FloatingPoint(const FloatingPointSize& size, negative, exactExp.signExtend(extension), sig); // Then cast... - d_fpl = new FloatingPointLiteral( - symfpu::convertFloatToFloat(exactFormat, size, rm, exactFloat.d_symuf)); + d_fpl.reset(new FloatingPointLiteral(symfpu::convertFloatToFloat( + exactFormat, size, rm, exactFloat.d_symuf))); #else Unreachable() << "no concrete implementation of FloatingPointLiteral"; #endif @@ -295,8 +295,6 @@ FloatingPoint::FloatingPoint(const FloatingPointSize& size, FloatingPoint::~FloatingPoint() { - delete d_fpl; - d_fpl = nullptr; } FloatingPoint FloatingPoint::makeNaN(const FloatingPointSize& size) diff --git a/src/util/floatingpoint.h b/src/util/floatingpoint.h index 754c38290..2d27b836e 100644 --- a/src/util/floatingpoint.h +++ b/src/util/floatingpoint.h @@ -20,6 +20,8 @@ #ifndef CVC4__FLOATINGPOINT_H #define CVC4__FLOATINGPOINT_H +#include + #include "util/bitvector.h" #include "util/floatingpoint_size.h" #include "util/rational.h" @@ -60,8 +62,6 @@ class CVC4_PUBLIC FloatingPoint /** Constructors. */ FloatingPoint(uint32_t e, uint32_t s, const BitVector& bv); FloatingPoint(const FloatingPointSize& size, const BitVector& bv); - FloatingPoint(const FloatingPointSize& fp_size, - const FloatingPointLiteral* fpl); FloatingPoint(const FloatingPoint& fp); FloatingPoint(const FloatingPointSize& size, const RoundingMode& rm, @@ -118,7 +118,7 @@ class CVC4_PUBLIC FloatingPoint static FloatingPoint makeMaxNormal(const FloatingPointSize& size, bool sign); /** Get the wrapped floating-point value. */ - const FloatingPointLiteral* getLiteral(void) const { return d_fpl; } + const FloatingPointLiteral* getLiteral(void) const { return d_fpl.get(); } /** * Return a string representation of this floating-point. @@ -258,8 +258,16 @@ class CVC4_PUBLIC FloatingPoint FloatingPointSize d_fp_size; private: + /** + * Constructor. + * + * Note: This constructor takes ownership of 'fpl' and is not intended for + * public use. + */ + FloatingPoint(const FloatingPointSize& fp_size, FloatingPointLiteral* fpl); + /** The floating-point literal of this floating-point value. */ - FloatingPointLiteral* d_fpl; + std::unique_ptr d_fpl; }; /* class FloatingPoint */ -- cgit v1.2.3 From 32f8874353e12f273212d153091f084617faea2e Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 30 Nov 2020 16:50:09 -0600 Subject: Use new let binding in AST printer (#5529) Required for removing the old DagificationVisitor --- src/printer/ast/ast_printer.cpp | 102 ++++++++++++++++++++++++++------------ src/printer/ast/ast_printer.h | 16 +++++- src/printer/smt2/smt2_printer.cpp | 1 - 3 files changed, 85 insertions(+), 34 deletions(-) diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp index 4b9371181..30b09acae 100644 --- a/src/printer/ast/ast_printer.cpp +++ b/src/printer/ast/ast_printer.cpp @@ -24,10 +24,9 @@ #include "expr/node_manager_attributes.h" // for VarNameAttr #include "expr/node_visitor.h" #include "options/language.h" // for LANG_AST -#include "printer/dagification_visitor.h" +#include "printer/let_binding.h" #include "smt/command.h" #include "smt/node_command.h" -#include "theory/substitutions.h" using namespace std; @@ -41,38 +40,17 @@ void AstPrinter::toStream(std::ostream& out, size_t dag) const { if(dag != 0) { - DagificationVisitor dv(dag); - NodeVisitor visitor; - visitor.run(dv, n); - const theory::SubstitutionMap& lets = dv.getLets(); - if(!lets.empty()) { - out << "(LET "; - bool first = true; - for(theory::SubstitutionMap::const_iterator i = lets.begin(); - i != lets.end(); - ++i) { - if(! first) { - out << ", "; - } else { - first = false; - } - toStream(out, (*i).second, toDepth, false); - out << " := "; - toStream(out, (*i).first, toDepth, false); - } - out << " IN "; - } - Node body = dv.getDagifiedBody(); - toStream(out, body, toDepth); - if(!lets.empty()) { - out << ')'; - } + LetBinding lbind(dag + 1); + toStreamWithLetify(out, n, toDepth, &lbind); } else { toStream(out, n, toDepth); } } -void AstPrinter::toStream(std::ostream& out, TNode n, int toDepth) const +void AstPrinter::toStream(std::ostream& out, + TNode n, + int toDepth, + LetBinding* lbind) const { // null if(n.getKind() == kind::NULL_EXPR) { @@ -96,12 +74,28 @@ void AstPrinter::toStream(std::ostream& out, TNode n, int toDepth) const // constant out << ' '; kind::metakind::NodeValueConstPrinter::toStream(out, n); - } else { + } + else if (n.isClosure()) + { + for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++) + { + // body is re-letified + if (i == 1) + { + toStreamWithLetify(out, n[i], toDepth, lbind); + continue; + } + toStream(out, n[i], toDepth < 0 ? toDepth : toDepth - 1, lbind); + } + } + else + { // operator if(n.getMetaKind() == kind::metakind::PARAMETERIZED) { out << ' '; if(toDepth != 0) { - toStream(out, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1); + toStream( + out, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1, lbind); } else { out << "(...)"; } @@ -114,7 +108,7 @@ void AstPrinter::toStream(std::ostream& out, TNode n, int toDepth) const out << ' '; } if(toDepth != 0) { - toStream(out, *i, toDepth < 0 ? toDepth : toDepth - 1); + toStream(out, *i, toDepth < 0 ? toDepth : toDepth - 1, lbind); } else { out << "(...)"; } @@ -394,6 +388,50 @@ void AstPrinter::toStreamCmdComment(std::ostream& out, out << "CommentCommand([" << comment << "])" << std::endl; } +void AstPrinter::toStreamWithLetify(std::ostream& out, + Node n, + int toDepth, + LetBinding* lbind) const +{ + if (lbind == nullptr) + { + toStream(out, n, toDepth); + return; + } + std::stringstream cparen; + std::vector letList; + lbind->letify(n, letList); + if (!letList.empty()) + { + std::map::const_iterator it; + out << "(LET "; + cparen << ")"; + bool first = true; + for (size_t i = 0, nlets = letList.size(); i < nlets; i++) + { + if (!first) + { + out << ", "; + } + else + { + first = false; + } + Node nl = letList[i]; + uint32_t id = lbind->getId(nl); + out << "_let_" << id << " := "; + Node nlc = lbind->convert(nl, "_let_", false); + toStream(out, nlc, toDepth, lbind); + } + out << " IN "; + } + Node nc = lbind->convert(n, "_let_"); + // print the body, passing the lbind object + toStream(out, nc, toDepth, lbind); + out << cparen.str(); + lbind->popScope(); +} + template static bool tryToStream(std::ostream& out, const Command* c) { diff --git a/src/printer/ast/ast_printer.h b/src/printer/ast/ast_printer.h index e4251eba0..e0bc7b6bf 100644 --- a/src/printer/ast/ast_printer.h +++ b/src/printer/ast/ast_printer.h @@ -24,6 +24,9 @@ #include "printer/printer.h" namespace CVC4 { + +class LetBinding; + namespace printer { namespace ast { @@ -162,7 +165,10 @@ class AstPrinter : public CVC4::Printer std::ostream& out, const std::vector& sequence) const override; private: - void toStream(std::ostream& out, TNode n, int toDepth) const; + void toStream(std::ostream& out, + TNode n, + int toDepth, + LetBinding* lbind = nullptr) const; /** * To stream model sort. This prints the appropriate output for type * tn declared via declare-sort or declare-datatype. @@ -178,6 +184,14 @@ class AstPrinter : public CVC4::Printer void toStreamModelTerm(std::ostream& out, const smt::Model& m, Node n) const override; + /** + * To stream with let binding. This prints n, possibly in the scope + * of letification generated by this method based on lbind. + */ + void toStreamWithLetify(std::ostream& out, + Node n, + int toDepth, + LetBinding* lbind) const; }; /* class AstPrinter */ } // namespace ast diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 9e9500bdb..d3e9b48e4 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -40,7 +40,6 @@ #include "theory/arrays/theory_arrays_rewriter.h" #include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/quantifiers_attributes.h" -#include "theory/substitutions.h" #include "theory/theory_model.h" #include "util/smt2_quote_string.h" -- cgit v1.2.3 From e7924fc22d220909c1b3eb0e41a1cdb624a69be7 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Mon, 30 Nov 2020 15:26:33 -0800 Subject: fp_converter: Properly separate out symbolic glue code. (#5501) File fp_converter.h encapsulates the symbolic glue code for symFPU and implements the actual word-blaster (class FpConverter). This header should not be included in any other headers in order to no pull in symFPU headers where it's not needed. However, it was included in src/theory/fp/theory_fp.h. This properly separates it out and does some clean up in TheoryFP, which still needs more love to conform to code style guidelines, and also more documentation. More love and documentation is postponed to future PRs to make reviewing easier. --- src/theory/fp/fp_converter.cpp | 8 +++-- src/theory/fp/fp_converter.h | 31 ++++++++--------- src/theory/fp/theory_fp.cpp | 45 +++++++++++++------------ src/theory/fp/theory_fp.h | 75 ++++++++++++++++++++++-------------------- 4 files changed, 85 insertions(+), 74 deletions(-) diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp index 85482bf6d..858710746 100644 --- a/src/theory/fp/fp_converter.cpp +++ b/src/theory/fp/fp_converter.cpp @@ -755,18 +755,20 @@ TypeNode floatingPointTypeInfo::getTypeNode(void) const } FpConverter::FpConverter(context::UserContext* user) - : + : d_additionalAssertions(user) #ifdef CVC4_USE_SYMFPU + , d_fpMap(user), d_rmMap(user), d_boolMap(user), d_ubvMap(user), - d_sbvMap(user), + d_sbvMap(user) #endif - d_additionalAssertions(user) { } +FpConverter::~FpConverter() {} + #ifdef CVC4_USE_SYMFPU Node FpConverter::ufToNode(const fpt &format, const uf &u) const { diff --git a/src/theory/fp/fp_converter.h b/src/theory/fp/fp_converter.h index e48d651bd..6688e8607 100644 --- a/src/theory/fp/fp_converter.h +++ b/src/theory/fp/fp_converter.h @@ -14,6 +14,8 @@ ** Uses the symfpu library to convert from floating-point operations to ** bit-vectors and propositions allowing the theory to be solved by ** 'bit-blasting'. + ** + ** !!! This header is not to be included in any other headers !!! **/ #include "cvc4_private.h" @@ -49,10 +51,6 @@ namespace CVC4 { namespace theory { namespace fp { -typedef PairHashFunction - PairTypeNodeHashFunction; - /** * This is a symfpu symbolic "back-end". It allows the library to be used to * construct bit-vector expressions that compute floating-point operations. @@ -302,6 +300,20 @@ class floatingPointTypeInfo : public FloatingPointSize */ class FpConverter { + public: + /** Constructor. */ + FpConverter(context::UserContext*); + /** Destructor. */ + ~FpConverter(); + + /** Adds a node to the conversion, returns the converted node */ + Node convert(TNode); + + /** Gives the node representing the value of a given variable */ + Node getValue(Valuation&, TNode); + + context::CDList d_additionalAssertions; + protected: #ifdef CVC4_USE_SYMFPU typedef symfpuSymbolic::traits traits; @@ -338,17 +350,6 @@ class FpConverter /* Creates the relevant components for a variable */ uf buildComponents(TNode current); #endif - - public: - context::CDList d_additionalAssertions; - - FpConverter(context::UserContext *); - - /** Adds a node to the conversion, returns the converted node */ - Node convert(TNode); - - /** Gives the node representing the value of a given variable */ - Node getValue(Valuation &, TNode); }; } // namespace fp diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index 0b15486e2..01fab92c8 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -23,6 +23,7 @@ #include #include "options/fp_options.h" +#include "theory/fp/fp_converter.h" #include "theory/fp/theory_fp_rewriter.h" #include "theory/rewriter.h" #include "theory/theory_model.h" @@ -108,7 +109,7 @@ TheoryFp::TheoryFp(context::Context* c, : Theory(THEORY_FP, c, u, out, valuation, logicInfo, pnm), d_notification(*this), d_registeredTerms(u), - d_conv(u), + d_conv(new FpConverter(u)), d_expansionRequested(false), d_conflictNode(c, Node::null()), d_minMap(u), @@ -116,9 +117,9 @@ TheoryFp::TheoryFp(context::Context* c, d_toUBVMap(u), d_toSBVMap(u), d_toRealMap(u), - realToFloatMap(u), - floatToRealMap(u), - abstractionMap(u), + d_realToFloatMap(u), + d_floatToRealMap(u), + d_abstractionMap(u), d_state(c, u, valuation) { // indicate we are using the default theory state object @@ -341,10 +342,10 @@ Node TheoryFp::abstractRealToFloat(Node node) Assert(t.getKind() == kind::FLOATINGPOINT_TYPE); NodeManager *nm = NodeManager::currentNM(); - ComparisonUFMap::const_iterator i(realToFloatMap.find(t)); + ComparisonUFMap::const_iterator i(d_realToFloatMap.find(t)); Node fun; - if (i == realToFloatMap.end()) + if (i == d_realToFloatMap.end()) { std::vector args(2); args[0] = node[0].getType(); @@ -353,7 +354,7 @@ Node TheoryFp::abstractRealToFloat(Node node) nm->mkFunctionType(args, node.getType()), "floatingpoint_abstract_real_to_float", NodeManager::SKOLEM_EXACT_NAME); - realToFloatMap.insert(t, fun); + d_realToFloatMap.insert(t, fun); } else { @@ -361,7 +362,7 @@ Node TheoryFp::abstractRealToFloat(Node node) } Node uf = nm->mkNode(kind::APPLY_UF, fun, node[0], node[1]); - abstractionMap.insert(uf, node); + d_abstractionMap.insert(uf, node); return uf; } @@ -373,10 +374,10 @@ Node TheoryFp::abstractFloatToReal(Node node) Assert(t.getKind() == kind::FLOATINGPOINT_TYPE); NodeManager *nm = NodeManager::currentNM(); - ComparisonUFMap::const_iterator i(floatToRealMap.find(t)); + ComparisonUFMap::const_iterator i(d_floatToRealMap.find(t)); Node fun; - if (i == floatToRealMap.end()) + if (i == d_floatToRealMap.end()) { std::vector args(2); args[0] = t; @@ -385,7 +386,7 @@ Node TheoryFp::abstractFloatToReal(Node node) nm->mkFunctionType(args, nm->realType()), "floatingpoint_abstract_float_to_real", NodeManager::SKOLEM_EXACT_NAME); - floatToRealMap.insert(t, fun); + d_floatToRealMap.insert(t, fun); } else { @@ -393,7 +394,7 @@ Node TheoryFp::abstractFloatToReal(Node node) } Node uf = nm->mkNode(kind::APPLY_UF, fun, node[0], node[1]); - abstractionMap.insert(uf, node); + d_abstractionMap.insert(uf, node); return uf; } @@ -737,9 +738,9 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete) void TheoryFp::convertAndEquateTerm(TNode node) { Trace("fp-convertTerm") << "TheoryFp::convertTerm(): " << node << std::endl; - size_t oldAdditionalAssertions = d_conv.d_additionalAssertions.size(); + size_t oldAdditionalAssertions = d_conv->d_additionalAssertions.size(); - Node converted(d_conv.convert(node)); + Node converted(d_conv->convert(node)); if (converted != node) { Debug("fp-convertTerm") @@ -748,11 +749,11 @@ void TheoryFp::convertAndEquateTerm(TNode node) { << "TheoryFp::convertTerm(): after " << converted << std::endl; } - size_t newAdditionalAssertions = d_conv.d_additionalAssertions.size(); + size_t newAdditionalAssertions = d_conv->d_additionalAssertions.size(); Assert(oldAdditionalAssertions <= newAdditionalAssertions); while (oldAdditionalAssertions < newAdditionalAssertions) { - Node addA = d_conv.d_additionalAssertions[oldAdditionalAssertions]; + Node addA = d_conv->d_additionalAssertions[oldAdditionalAssertions]; Debug("fp-convertTerm") << "TheoryFp::convertTerm(): additional assertion " << addA << std::endl; @@ -953,8 +954,8 @@ void TheoryFp::postCheck(Effort level) TheoryModel* m = getValuation().getModel(); bool lemmaAdded = false; - for (abstractionMapType::const_iterator i = abstractionMap.begin(); - i != abstractionMap.end(); + for (AbstractionMap::const_iterator i = d_abstractionMap.begin(); + i != d_abstractionMap.end(); ++i) { if (m->hasTerm((*i).first)) @@ -1016,7 +1017,7 @@ TrustNode TheoryFp::explain(TNode n) } Node TheoryFp::getModelValue(TNode var) { - return d_conv.getValue(d_valuation, var); + return d_conv->getValue(d_valuation, var); } bool TheoryFp::collectModelInfo(TheoryModel* m, @@ -1069,14 +1070,16 @@ bool TheoryFp::collectModelValues(TheoryModel* m, } for (std::set::const_iterator i(relevantVariables.begin()); - i != relevantVariables.end(); ++i) { + i != relevantVariables.end(); + ++i) + { TNode node = *i; Trace("fp-collectModelInfo") << "TheoryFp::collectModelInfo(): relevantVariable " << node << std::endl; - if (!m->assertEquality(node, d_conv.getValue(d_valuation, node), true)) + if (!m->assertEquality(node, d_conv->getValue(d_valuation, node), true)) { return false; } diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h index 42c009893..fe91a39bd 100644 --- a/src/theory/fp/theory_fp.h +++ b/src/theory/fp/theory_fp.h @@ -24,7 +24,6 @@ #include #include "context/cdo.h" -#include "theory/fp/fp_converter.h" #include "theory/fp/theory_fp_rewriter.h" #include "theory/theory.h" #include "theory/uf/equality_engine.h" @@ -33,7 +32,10 @@ namespace CVC4 { namespace theory { namespace fp { -class TheoryFp : public Theory { +class FpConverter; + +class TheoryFp : public Theory +{ public: /** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */ TheoryFp(context::Context* c, @@ -42,8 +44,9 @@ class TheoryFp : public Theory { Valuation valuation, const LogicInfo& logicInfo, ProofNodeManager* pnm = nullptr); + //--------------------------------- initialization - /** get the official theory rewriter of this theory */ + /** Get the official theory rewriter of this theory. */ TheoryRewriter* getTheoryRewriter() override; /** * Returns true if we need an equality engine. If so, we initialize the @@ -51,7 +54,7 @@ class TheoryFp : public Theory { * documentation in Theory::needsEqualityEngine. */ bool needsEqualityEngine(EeSetupInfo& esi) override; - /** finish initialization */ + /** Finish initialization. */ void finishInit() override; //--------------------------------- end initialization @@ -77,8 +80,10 @@ class TheoryFp : public Theory { Node getModelValue(TNode var) override; bool collectModelInfo(TheoryModel* m, const std::set& relevantTerms) override; - /** Collect model values in m based on the relevant terms given by - * relevantTerms */ + /** + * Collect model values in m based on the relevant terms given by + * relevantTerms. + */ bool collectModelValues(TheoryModel* m, const std::set& relevantTerms) override; @@ -87,7 +92,20 @@ class TheoryFp : public Theory { TrustNode explain(TNode n) override; protected: - /** Equality engine */ + using PairTypeNodeHashFunction = PairHashFunction; + /** Uninterpreted functions for undefined cases of non-total operators. */ + using ComparisonUFMap = + context::CDHashMap; + /** Uninterpreted functions for lazy handling of conversions. */ + using ConversionUFMap = context:: + CDHashMap, Node, PairTypeNodeHashFunction>; + using ConversionAbstractionMap = ComparisonUFMap; + using AbstractionMap = context::CDHashMap; + + /** Equality engine. */ class NotifyClass : public eq::EqualityEngineNotify { protected: TheoryFp& d_theorySolver; @@ -108,14 +126,15 @@ class TheoryFp : public Theory { NotifyClass d_notification; - /** General utility **/ + /** General utility. */ void registerTerm(TNode node); bool isRegistered(TNode node); context::CDHashSet d_registeredTerms; - /** Bit-blasting conversion */ - FpConverter d_conv; + /** The word-blaster. Translates FP -> BV. */ + std::unique_ptr d_conv; + bool d_expansionRequested; void convertAndEquateTerm(TNode node); @@ -133,44 +152,30 @@ class TheoryFp : public Theory { */ void conflictEqConstantMerge(TNode t1, TNode t2); - context::CDO d_conflictNode; - - typedef context::CDHashMap - ComparisonUFMap; - - ComparisonUFMap d_minMap; - ComparisonUFMap d_maxMap; + bool refineAbstraction(TheoryModel* m, TNode abstract, TNode concrete); Node minUF(Node); Node maxUF(Node); - typedef context::CDHashMap, Node, - PairTypeNodeHashFunction> - ConversionUFMap; - - ConversionUFMap d_toUBVMap; - ConversionUFMap d_toSBVMap; - Node toUBVUF(Node); Node toSBVUF(Node); - ComparisonUFMap d_toRealMap; - Node toRealUF(Node); - /** Uninterpretted functions for lazy handling of conversions */ - typedef ComparisonUFMap conversionAbstractionMap; - - conversionAbstractionMap realToFloatMap; - conversionAbstractionMap floatToRealMap; - Node abstractRealToFloat(Node); Node abstractFloatToReal(Node); - typedef context::CDHashMap abstractionMapType; - abstractionMapType abstractionMap; // abstract -> original + private: + context::CDO d_conflictNode; - bool refineAbstraction(TheoryModel* m, TNode abstract, TNode concrete); + ComparisonUFMap d_minMap; + ComparisonUFMap d_maxMap; + ConversionUFMap d_toUBVMap; + ConversionUFMap d_toSBVMap; + ComparisonUFMap d_toRealMap; + ConversionAbstractionMap d_realToFloatMap; + ConversionAbstractionMap d_floatToRealMap; + AbstractionMap d_abstractionMap; // abstract -> original /** The theory rewriter for this theory. */ TheoryFpRewriter d_rewriter; -- cgit v1.2.3 From acdffc72bd559fa4b64da2ee2b3373208354e7a1 Mon Sep 17 00:00:00 2001 From: yoni206 Date: Mon, 30 Nov 2020 18:42:19 -0800 Subject: fix metadata for a test (#5546) A COMMAND was used instead of COMMAND-LINE. --- test/regress/regress0/bv/bv_to_int_5281.smt2 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/regress/regress0/bv/bv_to_int_5281.smt2 b/test/regress/regress0/bv/bv_to_int_5281.smt2 index 4d0da1dbb..dc2cb7f35 100644 --- a/test/regress/regress0/bv/bv_to_int_5281.smt2 +++ b/test/regress/regress0/bv/bv_to_int_5281.smt2 @@ -1,4 +1,4 @@ -; COMMAND: --check-models --incremental +; COMMAND-LINE: --check-models --incremental ; EXPECT: sat (set-logic ALL) (set-option :check-models true) -- cgit v1.2.3 From 6489cf590b441aeb5e1bdf9800c9718d06842149 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 30 Nov 2020 22:22:24 -0600 Subject: More fixes for quantifier elimination (#5533) Fixes #5506, fixes #5507. --- src/smt/quant_elim_solver.cpp | 14 ++++++++++++-- src/smt/quant_elim_solver.h | 13 ++++++++++++- src/smt/smt_engine.cpp | 3 ++- src/theory/quantifiers_engine.cpp | 2 ++ test/regress/CMakeLists.txt | 2 ++ test/regress/regress1/quantifiers/issue5506-qe.smt2 | 6 ++++++ test/regress/regress1/quantifiers/issue5507-qe.smt2 | 19 +++++++++++++++++++ 7 files changed, 55 insertions(+), 4 deletions(-) create mode 100644 test/regress/regress1/quantifiers/issue5506-qe.smt2 create mode 100644 test/regress/regress1/quantifiers/issue5507-qe.smt2 diff --git a/src/smt/quant_elim_solver.cpp b/src/smt/quant_elim_solver.cpp index e5ecafd4a..4636cf17a 100644 --- a/src/smt/quant_elim_solver.cpp +++ b/src/smt/quant_elim_solver.cpp @@ -14,6 +14,7 @@ #include "smt/quant_elim_solver.h" +#include "expr/skolem_manager.h" #include "expr/subs.h" #include "smt/smt_solver.h" #include "theory/quantifiers/cegqi/nested_qe.h" @@ -33,7 +34,8 @@ QuantElimSolver::~QuantElimSolver() {} Node QuantElimSolver::getQuantifierElimination(Assertions& as, Node q, - bool doFull) + bool doFull, + bool isInternalSubsolver) { Trace("smt-qe") << "QuantElimSolver: get qe : " << q << std::endl; if (q.getKind() != EXISTS && q.getKind() != FORALL) @@ -41,11 +43,13 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as, throw ModalException( "Expecting a quantified formula as argument to get-qe."); } + NodeManager* nm = NodeManager::currentNM(); + // ensure the body is rewritten + q = nm->mkNode(q.getKind(), q[0], Rewriter::rewrite(q[1])); // do nested quantifier elimination if necessary q = quantifiers::NestedQe::doNestedQe(q, true); Trace("smt-qe") << "QuantElimSolver: after nested quantifier elimination : " << q << std::endl; - NodeManager* nm = NodeManager::currentNM(); // tag the quantified formula with the quant-elim attribute TypeNode t = nm->booleanType(); Node n_attr = nm->mkSkolem("qe", t, "Auxiliary variable for qe attr."); @@ -121,6 +125,12 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as, // do extended rewrite to minimize the size of the formula aggressively theory::quantifiers::ExtendedRewriter extr(true); ret = extr.extendedRewrite(ret); + // if we are not an internal subsolver, convert to witness form, since + // internally generated skolems should not escape + if (!isInternalSubsolver) + { + ret = SkolemManager::getWitnessForm(ret); + } return ret; } // otherwise, just true/false diff --git a/src/smt/quant_elim_solver.h b/src/smt/quant_elim_solver.h index 96ed1f73d..ca55fc618 100644 --- a/src/smt/quant_elim_solver.h +++ b/src/smt/quant_elim_solver.h @@ -79,8 +79,19 @@ class QuantElimSolver * extended command get-qe-disjunct, which can be used * for incrementally computing the result of a * quantifier elimination. + * + * @param as The assertions of the SmtEngine + * @param q The quantified formula we are eliminating quantifiers from + * @param doFull Whether we are doing full quantifier elimination on q + * @param isInternalSubsolver Whether the SmtEngine we belong to is an + * internal subsolver. If it is not, then we convert the final result to + * witness form. + * @return The result of eliminating quantifiers from q. */ - Node getQuantifierElimination(Assertions& as, Node q, bool doFull); + Node getQuantifierElimination(Assertions& as, + Node q, + bool doFull, + bool isInternalSubsolver); private: /** The SMT solver, which is used during doQuantifierElimination. */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 722f6a080..d3ba676fc 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1498,7 +1498,8 @@ Node SmtEngine::getQuantifierElimination(Node q, bool doFull, bool strict) if(!d_logic.isPure(THEORY_ARITH) && strict){ Warning() << "Unexpected logic for quantifier elimination " << d_logic << endl; } - return d_quantElimSolver->getQuantifierElimination(*d_asserts, q, doFull); + return d_quantElimSolver->getQuantifierElimination( + *d_asserts, q, doFull, d_isInternalSubsolver); } bool SmtEngine::getInterpol(const Node& conj, diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 297f11690..da9fdd022 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -336,6 +336,8 @@ bool QuantifiersEngine::getBoundElements(RepSetIterator* rsi, void QuantifiersEngine::presolve() { Trace("quant-engine-proc") << "QuantifiersEngine : presolve " << std::endl; + d_lemmas_waiting.clear(); + d_phase_req_waiting.clear(); for( unsigned i=0; ipresolve(); } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 816202fa9..4445a28d0 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1622,6 +1622,8 @@ set(regress_1_tests regress1/quantifiers/issue5482-rtf-no-fv.smt2 regress1/quantifiers/issue5484-qe.smt2 regress1/quantifiers/issue5484b-qe.smt2 + regress1/quantifiers/issue5506-qe.smt2 + regress1/quantifiers/issue5507-qe.smt2 regress1/quantifiers/issue993.smt2 regress1/quantifiers/javafe.ast.StmtVec.009.smt2 regress1/quantifiers/lia-witness-div-pp.smt2 diff --git a/test/regress/regress1/quantifiers/issue5506-qe.smt2 b/test/regress/regress1/quantifiers/issue5506-qe.smt2 new file mode 100644 index 000000000..3839f2d75 --- /dev/null +++ b/test/regress/regress1/quantifiers/issue5506-qe.smt2 @@ -0,0 +1,6 @@ +; SCRUBBER: sed 's/(.*)/()/g' +; EXPECT: () +; EXIT: 0 +(set-logic LIA) +(declare-fun a () Int) +(get-qe (forall ((b Int)) (= a 0))) diff --git a/test/regress/regress1/quantifiers/issue5507-qe.smt2 b/test/regress/regress1/quantifiers/issue5507-qe.smt2 new file mode 100644 index 000000000..3b7ddbcf3 --- /dev/null +++ b/test/regress/regress1/quantifiers/issue5507-qe.smt2 @@ -0,0 +1,19 @@ +; EXPECT: false +; EXIT: 0 +(set-logic LIA) +(declare-fun v0 () Bool) +(declare-fun v1 () Bool) +(declare-fun v2 () Bool) +(declare-fun v3 () Bool) +(declare-fun v5 () Bool) +(declare-fun v6 () Bool) +(declare-fun v9 () Bool) +(declare-fun v10 () Bool) +(declare-fun v15 () Bool) +(declare-fun v16 () Bool) +(declare-fun i0 () Int) +(declare-fun i2 () Int) +(declare-fun i9 () Int) +(declare-fun v26 () Bool) +(declare-fun v33 () Bool) +(get-qe (exists ((q154 Bool) (q155 Int) (q156 Bool) (q157 Bool) (q158 Bool) (q159 Bool) (q160 Int)) (and (=> (distinct 309 i2) (or q157 v9 (distinct v16 v6 v5 v10) q159 (=> v15 v26))) (exists ((q154 Bool) (q155 Int) (q156 Bool) (q157 Bool) (q158 Bool) (q159 Bool) (q160 Int)) (=> (xor q156 v3 v2 q156 q156 q159 (>= 217 826 149 i0 i9) v1 v5 q157 q157) (distinct q160 q160))) v33 (distinct v16 v6 v5 v10) v0))) -- cgit v1.2.3 From d452621ef035a0127d691618e85a4fa2ab6fa027 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Tue, 1 Dec 2020 15:03:50 +0100 Subject: Add regressions for #4707. (#5555) The error from #4707 has been fixed in the meantime, this PR adds the example inputs as regressions. Closes #4707. --- test/regress/CMakeLists.txt | 2 + .../regress0/issue4707-bv-to-bool-small.smt2 | 13 +++ .../regress2/issue4707-bv-to-bool-large.smt2 | 129 +++++++++++++++++++++ 3 files changed, 144 insertions(+) create mode 100644 test/regress/regress0/issue4707-bv-to-bool-small.smt2 create mode 100644 test/regress/regress2/issue4707-bv-to-bool-large.smt2 diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 4445a28d0..9662ea094 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -584,6 +584,7 @@ set(regress_0_tests regress0/issue2832-qualId.smt2 regress0/issue4010-sort-inf-var.smt2 regress0/issue4469-unc-no-reuse-var.smt2 + regress0/issue4707-bv-to-bool-small.smt2 regress0/issue5144-resetAssertions.smt2 regress0/ite.cvc regress0/ite2.smt2 @@ -2169,6 +2170,7 @@ set(regress_2_tests regress2/hole7.cvc regress2/hole8.cvc regress2/instance_1444.smtv1.smt2 + regress2/issue4707-bv-to-bool-large.smt2 regress2/javafe.ast.StandardPrettyPrint.319_no_forall.smt2 regress2/javafe.ast.WhileStmt.447_no_forall.smt2 regress2/ooo.rf6.smt2 diff --git a/test/regress/regress0/issue4707-bv-to-bool-small.smt2 b/test/regress/regress0/issue4707-bv-to-bool-small.smt2 new file mode 100644 index 000000000..c2f0a58ad --- /dev/null +++ b/test/regress/regress0/issue4707-bv-to-bool-small.smt2 @@ -0,0 +1,13 @@ +; EXPECT: sat +(set-logic ALL) +(declare-fun b () (Array (_ BitVec 10) (_ BitVec 1))) +(declare-fun c () (Array (_ BitVec 10) (_ BitVec 1))) +(declare-fun ae () (_ BitVec 10)) +(declare-fun ag () (_ BitVec 10)) +(declare-fun ak () (_ BitVec 10)) +(assert (= (_ bv1 1) (bvand (bvcomp ae ((_ zero_extend 9) (select b (_ bv0 + 10)))) (bvsdiv (bvcomp ae ak) (bvand (ite (= (_ bv0 1) (bvcomp ag (bvshl ((_ + zero_extend 9) (select c (bvadd ae (_ bv3 10)))) (_ bv8 10)))) (_ bv1 1) (_ + bv0 1)) (ite (= b (store (store c (bvadd ae (_ bv3 10)) ((_ extract 0 0) + (bvlshr ag (_ bv8 10)))) ak (_ bv1 1))) (_ bv1 1) (_ bv0 1))))))) +(check-sat) \ No newline at end of file diff --git a/test/regress/regress2/issue4707-bv-to-bool-large.smt2 b/test/regress/regress2/issue4707-bv-to-bool-large.smt2 new file mode 100644 index 000000000..bb4e9794c --- /dev/null +++ b/test/regress/regress2/issue4707-bv-to-bool-large.smt2 @@ -0,0 +1,129 @@ +; EXPECT: sat +(set-logic ALL) +(declare-fun a () (Array (_ BitVec 32) (_ BitVec 8))) +(declare-fun b () (Array (_ BitVec 32) (_ BitVec 8))) +(declare-fun c () (Array (_ BitVec 32) (_ BitVec 8))) +(declare-fun d () (Array (_ BitVec 32) (_ BitVec 8))) +(declare-fun aa () (_ BitVec 1)) +(declare-fun e () (_ BitVec 1)) +(declare-fun f () (_ BitVec 1)) +(declare-fun ab () (_ BitVec 1)) +(declare-fun g () (_ BitVec 1)) +(declare-fun h () (_ BitVec 1)) +(declare-fun i () (_ BitVec 1)) +(declare-fun j () (_ BitVec 1)) +(declare-fun k () (_ BitVec 1)) +(declare-fun l () (_ BitVec 1)) +(declare-fun m () (_ BitVec 1)) +(declare-fun n () (_ BitVec 1)) +(declare-fun o () (_ BitVec 1)) +(declare-fun p () (_ BitVec 1)) +(declare-fun q () (_ BitVec 1)) +(declare-fun r () (_ BitVec 1)) +(declare-fun s () (_ BitVec 1)) +(declare-fun t () (_ BitVec 1)) +(declare-fun u () (_ BitVec 1)) +(declare-fun v () (_ BitVec 1)) +(declare-fun w () (_ BitVec 1)) +(declare-fun x () (_ BitVec 1)) +(declare-fun y () (_ BitVec 1)) +(declare-fun z () (_ BitVec 1)) +(declare-fun ac () (_ BitVec 1)) +(declare-fun ad () (_ BitVec 32)) +(declare-fun ae () (_ BitVec 32)) +(declare-fun af () (_ BitVec 32)) +(declare-fun ag () (_ BitVec 32)) +(declare-fun ah () (_ BitVec 32)) +(declare-fun ai () (_ BitVec 32)) +(declare-fun aj () (_ BitVec 32)) +(declare-fun ak () (_ BitVec 32)) +(declare-fun al () (_ BitVec 32)) +(declare-fun am () (_ BitVec 32)) +(declare-fun an () (_ BitVec 32)) +(declare-fun ao () (_ BitVec 1)) +(declare-fun ap () (_ BitVec 32)) +(declare-fun aq () (_ BitVec 1)) +(declare-fun ar () (_ BitVec 32)) +(declare-fun au () (_ BitVec 32)) +(declare-fun av () (_ BitVec 32)) +(declare-fun aw () (_ BitVec 32)) +(declare-fun ax () (_ BitVec 32)) +(declare-fun ay () (_ BitVec 32)) +(assert + (let ((?as (bvadd av (_ bv4 32))) + (?at (bvadd av (_ bv12 32)))) + (= (_ bv1 1) (bvand (bvand (ite (= ac (ite (= an ai) (_ bv1 1) (_ + bv0 1))) (_ bv1 1) (_ bv0 1)) (bvmul (ite (= z (ite (= ai aj) (_ + bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= y (ite (= aj + (bvor (bvnand (bvor (concat (_ bv0 24) (select d (bvadd ak (_ bv0 + 32)))) (bvshl (concat (_ bv0 24) (select d (bvadd ak (_ bv1 32)))) + (_ bv8 32))) (bvshl (concat (_ bv0 24) (select d (bvadd ak (_ bv2 + 32)))) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select d (bvadd ak + (_ bv3 32)))) (_ bv24 32)))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 + 1)) (bvand (ite (= x (ite (= ak ?as) (_ bv1 1) (_ bv0 1))) (_ bv1 + 1) (_ bv0 1)) (bvand (ite (= w (ite (= d (store (store (store + (store c (bvadd (_ bv134533664 32) (_ bv3 32)) ((_ extract 7 0) + (bvlshr al (_ bv24 32)))) (bvadd (_ bv134533664 32) (_ bv2 32)) ((_ + extract 7 0) (bvlshr al (_ bv16 32)))) (bvadd (_ bv134533664 32) (_ + bv1 32)) ((_ extract 7 0) (bvlshr al (_ bv8 32)))) (bvadd (_ + bv134533664 32) (_ bv0 32)) ((_ extract 7 0) al))) (_ bv1 1) (_ bv0 + 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= v (ite (= al (bvor (bvor + (bvor (concat (_ bv0 24) (select c (bvadd am (_ bv0 32)))) (bvshl + (concat (_ bv0 24) (select c (bvadd am (_ bv1 32)))) (_ bv8 32))) + (bvshl (concat (_ bv0 24) (select c (bvadd am (_ bv2 32)))) (_ bv16 + 32))) (bvshl (concat (_ bv0 24) (select c (bvsub am (_ bv3 32)))) + (_ bv24 32)))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand + (ite (= u (ite (= am ?at) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 + 1)) (bvand (ite (= t ao) (_ bv1 1) (_ bv0 1)) (bvand (ite (= s (ite + (= an ad) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= + r (ite (= ad ae) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand + (ite (= q (ite (= ae (bvor (bvor (bvor (concat (_ bv0 24) (select b + (bvadd af (_ bv0 32)))) (bvxor (concat (_ bv0 24) (select b (bvadd + af (_ bv1 32)))) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select b + (bvadd af (_ bv2 32)))) (_ bv16 32))) (bvshl (concat (_ bv0 24) + (select b (bvadd af (_ bv3 32)))) (_ bv24 32)))) (_ bv1 1) (_ bv0 + 1))) (_ bv1 1) (_ bv0 1)) (bvsdiv (ite (= p (ite (= af ?as) (_ bv1 + 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= o (ite (= b + (store (store (store (store c (bvadd ar (_ bv3 32)) ((_ extract 7 + 0) (bvlshr ag (_ bv24 32)))) (bvadd ar (_ bv2 32)) ((_ extract 7 0) + (bvlshr ag (_ bv16 32)))) (bvand ar (_ bv1 32)) ((_ extract 7 0) + (bvlshr ag (_ bv8 32)))) (bvadd ar (_ bv0 32)) ((_ extract 7 0) + ag))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= n + (ite (= ag (bvor (bvor (bvor (concat (_ bv0 24) (select c (bvadd ah + (_ bv0 32)))) (bvshl (concat (_ bv0 24) (select c (bvadd ah (_ bv1 + 32)))) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select c (bvurem ah + (_ bv2 32)))) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select c + (bvadd ah (_ bv3 32)))) (_ bv24 32)))) (_ bv1 1) (_ bv0 1))) (_ bv1 + 1) (_ bv0 1)) (bvand (ite (= m (ite (= ah ?at) (_ bv1 1) (_ bv0 + 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= l ao ) (_ bv1 1) (_ bv0 + 1)) (bvand (ite (= k (bvor (bvand t (bvand u (bvand v (bvand w + (bvand x (bvand y (bvand z ac))))))) (bvand l (bvand m (bvand n + (bvand o (bvand p (bvand q (bvand r s))))))))) (_ bv1 1) (_ bv0 1)) + (bvand (ite (= j (ite (= ao ((_ extract 0 0) ap)) (_ bv1 1) (_ bv0 + 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= i (ite (= ap (concat (_ + bv0 31) aq)) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite + (= h (ite (= aq (ite (= ar (_ bv0 32)) (_ bv1 1) (_ bv0 1))) (_ bv1 + 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= g (ite (= ar + (bvor (bvor (bvor (concat (_ bv0 24) (select c (bvadd au (_ bv0 + 32)))) (bvshl (concat (_ bv0 24) (select c (bvadd au (_ bv1 32)))) + (_ bv8 32))) (bvshl (concat (_ bv0 24) (select c (bvadd au (_ bv2 + 32)))) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select c (bvadd au + (_ bv3 32)))) (_ bv24 32)))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 + 1)) (bvand (ite (= ab (ite (= au (bvadd av (_ bv8 32))) (_ bv1 1) + (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= f (ite (= c (store + (store (store (store a (bvadd av (_ bv3 32)) ((_ extract 7 0) + (bvlshr ay (_ bv24 32)))) (bvadd av (_ bv2 32)) ((_ extract 7 0) + (bvlshr ay (_ bv16 32)))) (bvadd av (_ bv1 32)) ((_ extract 7 0) + (bvlshr ay (_ bv8 32)))) (bvadd av (_ bv0 32)) ((_ extract 7 0) + ay))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= e + (ite (= av (bvsub ax (_ bv4 32))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) + (_ bv0 1)) (ite (= aa (ite (= aw (bvor (bvor (bvor (concat (_ bv0 + 24) (select a (bvadd ax (_ bv0 32)))) (bvshl (concat (_ bv0 24) + (select a (bvadd ax (_ bv1 32)))) (_ bv8 32))) (bvshl (concat (_ + bv0 24) (select a (bvadd ax (_ bv2 32)))) (_ bv16 32))) (bvshl + (concat (_ bv0 24) (select a (bvadd ax (_ bv3 32)))) (_ bv24 32)))) + (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)))))))))))))))))))))))))) + (bvand (bvnot (_ bv0 1)) (bvand (bvand aa (bvand e (bvand f (bvand + ab (bvand g (bvand h (bvand i (bvand j k)))))))) (ite (= aw an) (_ + bv1 1) (_ bv0 1)))))))) +(check-sat) \ No newline at end of file -- cgit v1.2.3 From 7fb5354114c7e17260b3ff520decf340734d52fe Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Tue, 1 Dec 2020 15:36:37 +0100 Subject: Add regression for #4335. (#5554) The error from #4335 has been fixed in the meantime, this PR adds a regression for this issue. Closes #4335. --- test/regress/CMakeLists.txt | 1 + test/regress/regress1/issue4335-unsat-core.smt2 | 187 ++++++++++++++++++++++++ 2 files changed, 188 insertions(+) create mode 100644 test/regress/regress1/issue4335-unsat-core.smt2 diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 9662ea094..6c064833a 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1417,6 +1417,7 @@ set(regress_1_tests regress1/issue3970-nl-ext-purify.smt2 regress1/issue3990-sort-inference.smt2 regress1/issue4273-ext-rew-cache.smt2 + regress1/issue4335-unsat-core.smt2 regress1/lemmas/clocksynchro_5clocks.main_invar.base.smtv1.smt2 regress1/lemmas/pursuit-safety-8.smtv1.smt2 regress1/lemmas/simple_startup_9nodes.abstract.base.smtv1.smt2 diff --git a/test/regress/regress1/issue4335-unsat-core.smt2 b/test/regress/regress1/issue4335-unsat-core.smt2 new file mode 100644 index 000000000..11e689515 --- /dev/null +++ b/test/regress/regress1/issue4335-unsat-core.smt2 @@ -0,0 +1,187 @@ +; SCRUBBER: sed -e 's/IP_[0-9]*/IP/' +; EXPECT: unsat +; EXPECT: ( +; EXPECT: IP +; EXPECT: IP +; EXPECT: IP +; EXPECT: IP +; EXPECT: IP +; EXPECT: IP +; EXPECT: IP +; EXPECT: IP +; EXPECT: IP +; EXPECT: ) +(set-logic ALL) +(set-option :produce-unsat-cores true) +(declare-const v0 Bool) +(declare-const v1 Bool) +(declare-const v2 Bool) +(declare-const v3 Bool) +(declare-const v4 Bool) +(declare-const i1 Int) +(declare-const r1 Real) +(declare-const r2 Real) +(declare-const r3 Real) +(declare-const r7 Real) +(declare-const r10 Real) +(declare-const r14 Real) +(declare-const r16 Real) +(declare-const r17 Real) +(declare-const r18 Real) +(declare-const v5 Bool) +(declare-const r20 Real) +(declare-const arr-5074471134850140881_778238581772319464-0 (Array Bool Int)) +(assert (! (exists ((q0 Int) (q1 Real) (q2 Int)) (not (> (- i1) (select (store arr-5074471134850140881_778238581772319464-0 v0 60) (= v0 v4 v3 v3 v4))))) :named IP_1)) +(assert (! (or (forall ((q0 Int) (q1 Real) (q2 Int)) (=> (>= r20 q1 q1 26271062.0) (<= q2 q2))) (exists ((q0 Int) (q1 Real) (q2 Int)) (=> (>= (- i1) q2) (< q1 q1 5851734.0)))) :named IP_2)) +(declare-const arr-778238581772319464_-3713212254555730767-0 (Array Int (_ BitVec 8))) +(declare-const v6 Bool) +(declare-const v7 Bool) +(declare-const arr--5101604640448673848_-3713212254554648242-0 (Array Real (_ BitVec 9))) +(declare-const arr--3713212254557895817_-5101604640448673848-0 (Array (_ BitVec 10) Real)) +(assert (! (or (distinct (- i1) 35) (not v4) (= v0 v4 v3 v3 v4)) :named IP_3)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) v0 (= v0 v4 v3 v3 v4)) :named IP_4)) +(assert (! (or (= v0 v4 v3 v3 v4) (distinct v4 (= v0 v4 v3 v3 v4)) (not v4)) :named IP_5)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) v3 (= v0 v4 v3 v3 v4)) :named IP_6)) +(assert (! (or (= v0 v4 v3 v3 v4) v3 (= v0 v4 v3 v3 v4)) :named IP_7)) +(assert (! (or (is_int 1193124502.0) (= v0 v4 v3 v3 v4) (not v4)) :named IP_8)) +(assert (! (or (= v0 v4 v3 v3 v4) (= v0 v4 v3 v3 v4) v0) :named IP_9)) +(assert (! (or (< 397 (div (- i1) 60)) v3 (= v0 v4 v3 v3 v4)) :named IP_10)) +(assert (! (or v3 v3 v3) :named IP_11)) +(assert (! (or (is_int 1193124502.0) (not v4) (= v0 v4 v3 v3 v4)) :named IP_12)) +(assert (! (or (< 397 (div (- i1) 60)) (is_int 1193124502.0) (distinct (- i1) 35)) :named IP_13)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (distinct (- i1) 35) v0) :named IP_14)) +(assert (! (or (is_int 1193124502.0) v0 (not v4)) :named IP_15)) +(assert (! (or (< 397 (div (- i1) 60)) (< 397 (div (- i1) 60)) (< 397 (div (- i1) 60))) :named IP_16)) +(assert (! (or (not v4) (distinct v4 (= v0 v4 v3 v3 v4)) (distinct (- i1) 35)) :named IP_17)) +(assert (! (or (distinct (- i1) 35) (= v0 v4 v3 v3 v4) (= v0 v4 v3 v3 v4)) :named IP_18)) +(assert (! (or v3 (distinct v4 (= v0 v4 v3 v3 v4)) (distinct v4 (= v0 v4 v3 v3 v4))) :named IP_19)) +(assert (! (or (= v0 v4 v3 v3 v4) (= v0 v4 v3 v3 v4) (is_int 1193124502.0)) :named IP_20)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (< 397 (div (- i1) 60)) (distinct v4 (= v0 v4 v3 v3 v4))) :named IP_21)) +(assert (! (or (< 397 (div (- i1) 60)) (distinct (- i1) 35) (= v0 v4 v3 v3 v4)) :named IP_22)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) v3 (is_int 1193124502.0)) :named IP_23)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (distinct (- i1) 35) (= v0 v4 v3 v3 v4)) :named IP_24)) +(assert (! (or (= v0 v4 v3 v3 v4) (is_int 1193124502.0) (< 397 (div (- i1) 60))) :named IP_25)) +(assert (! (or v0 v0 (= v0 v4 v3 v3 v4)) :named IP_26)) +(assert (! (or v0 (not v4) (= v0 v4 v3 v3 v4)) :named IP_27)) +(assert (! (or (= v0 v4 v3 v3 v4) v3 v3) :named IP_28)) +(assert (! (or v3 (= v0 v4 v3 v3 v4) (= v0 v4 v3 v3 v4)) :named IP_29)) +(assert (! (or (is_int 1193124502.0) (is_int 1193124502.0) (distinct (- i1) 35)) :named IP_30)) +(assert (! (or (distinct (- i1) 35) (not v4) (distinct (- i1) 35)) :named IP_31)) +(assert (! (or (= v0 v4 v3 v3 v4) (< 397 (div (- i1) 60)) v3) :named IP_32)) +(assert (! (or (= v0 v4 v3 v3 v4) (distinct (- i1) 35) (not v4)) :named IP_33)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) v0 v0) :named IP_34)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (distinct (- i1) 35) (< 397 (div (- i1) 60))) :named IP_35)) +(assert (! (or (= v0 v4 v3 v3 v4) (is_int 1193124502.0) (not v4)) :named IP_36)) +(assert (! (or (= v0 v4 v3 v3 v4) (distinct (- i1) 35) v0) :named IP_37)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (< 397 (div (- i1) 60)) (< 397 (div (- i1) 60))) :named IP_38)) +(assert (! (or (distinct (- i1) 35) v3 (= v0 v4 v3 v3 v4)) :named IP_39)) +(assert (! (or (< 397 (div (- i1) 60)) (is_int 1193124502.0) (not v4)) :named IP_40)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) v3 (is_int 1193124502.0)) :named IP_41)) +(assert (! (or v0 (distinct (- i1) 35) v0) :named IP_42)) +(assert (! (or (not v4) v0 (not v4)) :named IP_43)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (not v4) (= v0 v4 v3 v3 v4)) :named IP_44)) +(assert (! (or (is_int 1193124502.0) (distinct v4 (= v0 v4 v3 v3 v4)) (is_int 1193124502.0)) :named IP_45)) +(assert (! (or v0 (is_int 1193124502.0) (distinct (- i1) 35)) :named IP_46)) +(assert (! (or (= v0 v4 v3 v3 v4) v0 (distinct v4 (= v0 v4 v3 v3 v4))) :named IP_47)) +(assert (! (or (is_int 1193124502.0) v0 (= v0 v4 v3 v3 v4)) :named IP_48)) +(assert (! (or v0 (< 397 (div (- i1) 60)) v3) :named IP_49)) +(assert (! (or v0 v3 (is_int 1193124502.0)) :named IP_50)) +(assert (! (or v3 (distinct (- i1) 35) v0) :named IP_51)) +(assert (! (or v3 (distinct v4 (= v0 v4 v3 v3 v4)) (is_int 1193124502.0)) :named IP_52)) +(assert (! (or (is_int 1193124502.0) (distinct v4 (= v0 v4 v3 v3 v4)) (not v4)) :named IP_53)) +(assert (! (or (= v0 v4 v3 v3 v4) (< 397 (div (- i1) 60)) (distinct (- i1) 35)) :named IP_54)) +(assert (! (or (distinct (- i1) 35) v3 (not v4)) :named IP_55)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (distinct (- i1) 35) v0) :named IP_56)) +(assert (! (or (= v0 v4 v3 v3 v4) (< 397 (div (- i1) 60)) (distinct (- i1) 35)) :named IP_57)) +(assert (! (or (not v4) v0 (< 397 (div (- i1) 60))) :named IP_58)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (distinct (- i1) 35) (not v4)) :named IP_59)) +(assert (! (or (= v0 v4 v3 v3 v4) (distinct (- i1) 35) (is_int 1193124502.0)) :named IP_60)) +(assert (! (or (is_int 1193124502.0) v0 (distinct (- i1) 35)) :named IP_61)) +(assert (! (or (not v4) (< 397 (div (- i1) 60)) v3) :named IP_62)) +(assert (! (or (not v4) (distinct (- i1) 35) v0) :named IP_63)) +(assert (! (or (distinct (- i1) 35) (is_int 1193124502.0) v3) :named IP_64)) +(assert (! (or (= v0 v4 v3 v3 v4) (distinct v4 (= v0 v4 v3 v3 v4)) (= v0 v4 v3 v3 v4)) :named IP_65)) +(assert (! (or (< 397 (div (- i1) 60)) v3 v3) :named IP_66)) +(assert (! (or (not v4) v3 (distinct (- i1) 35)) :named IP_67)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) v3 v3) :named IP_68)) +(assert (! (or (distinct (- i1) 35) (distinct (- i1) 35) v0) :named IP_69)) +(assert (! (or v3 (not v4) (< 397 (div (- i1) 60))) :named IP_70)) +(assert (! (or (< 397 (div (- i1) 60)) (is_int 1193124502.0) (< 397 (div (- i1) 60))) :named IP_71)) +(assert (! (or (< 397 (div (- i1) 60)) (= v0 v4 v3 v3 v4) (= v0 v4 v3 v3 v4)) :named IP_72)) +(assert (! (or (is_int 1193124502.0) (distinct v4 (= v0 v4 v3 v3 v4)) (not v4)) :named IP_73)) +(assert (! (or v0 v0 (is_int 1193124502.0)) :named IP_74)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (= v0 v4 v3 v3 v4) (distinct v4 (= v0 v4 v3 v3 v4))) :named IP_75)) +(assert (! (or v3 (not v4) v0) :named IP_76)) +(assert (! (or (< 397 (div (- i1) 60)) (distinct v4 (= v0 v4 v3 v3 v4)) (not v4)) :named IP_77)) +(assert (! (or v3 (is_int 1193124502.0) (< 397 (div (- i1) 60))) :named IP_78)) +(assert (! (or (is_int 1193124502.0) (not v4) v0) :named IP_79)) +(assert (! (or (not v4) v3 (not v4)) :named IP_80)) +(assert (! (or v3 v0 v0) :named IP_81)) +(assert (! (or (= v0 v4 v3 v3 v4) (= v0 v4 v3 v3 v4) (is_int 1193124502.0)) :named IP_82)) +(assert (! (or (is_int 1193124502.0) (= v0 v4 v3 v3 v4) (not v4)) :named IP_83)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (is_int 1193124502.0) v0) :named IP_84)) +(assert (! (or (not v4) (distinct v4 (= v0 v4 v3 v3 v4)) (distinct v4 (= v0 v4 v3 v3 v4))) :named IP_85)) +(assert (! (or (= v0 v4 v3 v3 v4) v0 (= v0 v4 v3 v3 v4)) :named IP_86)) +(assert (! (or v3 (distinct (- i1) 35) (not v4)) :named IP_87)) +(assert (! (or (distinct (- i1) 35) v0 (not v4)) :named IP_88)) +(assert (! (or (distinct (- i1) 35) (< 397 (div (- i1) 60)) (distinct (- i1) 35)) :named IP_89)) +(assert (! (or (distinct (- i1) 35) (< 397 (div (- i1) 60)) (not v4)) :named IP_90)) +(assert (! (or (= v0 v4 v3 v3 v4) (is_int 1193124502.0) (distinct (- i1) 35)) :named IP_91)) +(assert (! (or (is_int 1193124502.0) (< 397 (div (- i1) 60)) (distinct (- i1) 35)) :named IP_92)) +(assert (! (or v0 (distinct (- i1) 35) (is_int 1193124502.0)) :named IP_93)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (distinct (- i1) 35) (= v0 v4 v3 v3 v4)) :named IP_94)) +(assert (! (or (= v0 v4 v3 v3 v4) (distinct (- i1) 35) (= v0 v4 v3 v3 v4)) :named IP_95)) +(assert (! (or v3 (not v4) (is_int 1193124502.0)) :named IP_96)) +(assert (! (or (is_int 1193124502.0) (distinct v4 (= v0 v4 v3 v3 v4)) (distinct v4 (= v0 v4 v3 v3 v4))) :named IP_97)) +(assert (! (or (= v0 v4 v3 v3 v4) v3 (distinct v4 (= v0 v4 v3 v3 v4))) :named IP_98)) +(assert (! (or (distinct (- i1) 35) (distinct v4 (= v0 v4 v3 v3 v4)) v3) :named IP_99)) +(assert (! (or v0 v0 (= v0 v4 v3 v3 v4)) :named IP_100)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (= v0 v4 v3 v3 v4) (= v0 v4 v3 v3 v4)) :named IP_101)) +(assert (! (or (is_int 1193124502.0) (= v0 v4 v3 v3 v4) (= v0 v4 v3 v3 v4)) :named IP_102)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (distinct v4 (= v0 v4 v3 v3 v4)) (= v0 v4 v3 v3 v4)) :named IP_103)) +(assert (! (or (not v4) (not v4) (= v0 v4 v3 v3 v4)) :named IP_104)) +(assert (! (or (< 397 (div (- i1) 60)) (distinct v4 (= v0 v4 v3 v3 v4)) (distinct (- i1) 35)) :named IP_105)) +(assert (! (or (= v0 v4 v3 v3 v4) (< 397 (div (- i1) 60)) (is_int 1193124502.0)) :named IP_106)) +(assert (! (or v0 (is_int 1193124502.0) (distinct (- i1) 35)) :named IP_107)) +(assert (! (or (< 397 (div (- i1) 60)) (= v0 v4 v3 v3 v4) (= v0 v4 v3 v3 v4)) :named IP_108)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) v3 (distinct (- i1) 35)) :named IP_109)) +(assert (! (or (= v0 v4 v3 v3 v4) v0 (not v4)) :named IP_110)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (= v0 v4 v3 v3 v4) (is_int 1193124502.0)) :named IP_111)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (= v0 v4 v3 v3 v4) (distinct (- i1) 35)) :named IP_112)) +(assert (! (or v0 (not v4) (< 397 (div (- i1) 60))) :named IP_113)) +(assert (! (or v3 (distinct (- i1) 35) v0) :named IP_114)) +(assert (! (or (< 397 (div (- i1) 60)) (distinct v4 (= v0 v4 v3 v3 v4)) (distinct v4 (= v0 v4 v3 v3 v4))) :named IP_115)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (distinct v4 (= v0 v4 v3 v3 v4)) (distinct (- i1) 35)) :named IP_116)) +(assert (! (or (< 397 (div (- i1) 60)) (is_int 1193124502.0) (not v4)) :named IP_117)) +(assert (! (or v0 (< 397 (div (- i1) 60)) (distinct v4 (= v0 v4 v3 v3 v4))) :named IP_118)) +(assert (! (or (distinct (- i1) 35) (= v0 v4 v3 v3 v4) (= v0 v4 v3 v3 v4)) :named IP_119)) +(assert (! (or (= v0 v4 v3 v3 v4) (is_int 1193124502.0) (distinct v4 (= v0 v4 v3 v3 v4))) :named IP_120)) +(assert (! (or v3 v3 v3) :named IP_121)) +(assert (! (or (is_int 1193124502.0) (< 397 (div (- i1) 60)) v3) :named IP_122)) +(assert (! (or (= v0 v4 v3 v3 v4) (= v0 v4 v3 v3 v4) (distinct v4 (= v0 v4 v3 v3 v4))) :named IP_123)) +(assert (! (or (not v4) (= v0 v4 v3 v3 v4) v3) :named IP_124)) +(assert (! (or (distinct (- i1) 35) (< 397 (div (- i1) 60)) (< 397 (div (- i1) 60))) :named IP_125)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (distinct (- i1) 35) (not v4)) :named IP_126)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) v0 v0) :named IP_127)) +(assert (! (or (is_int 1193124502.0) (distinct (- i1) 35) (is_int 1193124502.0)) :named IP_128)) +(assert (! (or v0 (= v0 v4 v3 v3 v4) (= v0 v4 v3 v3 v4)) :named IP_129)) +(assert (! (or v0 (distinct (- i1) 35) v0) :named IP_130)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (= v0 v4 v3 v3 v4) (is_int 1193124502.0)) :named IP_131)) +(assert (! (or (not v4) v3 (distinct (- i1) 35)) :named IP_132)) +(assert (! (or v0 (< 397 (div (- i1) 60)) (= v0 v4 v3 v3 v4)) :named IP_133)) +(assert (! (or (is_int 1193124502.0) (distinct v4 (= v0 v4 v3 v3 v4)) (< 397 (div (- i1) 60))) :named IP_134)) +(assert (! (or v0 (distinct v4 (= v0 v4 v3 v3 v4)) (is_int 1193124502.0)) :named IP_135)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (< 397 (div (- i1) 60)) (distinct v4 (= v0 v4 v3 v3 v4))) :named IP_136)) +(assert (! (or v3 (= v0 v4 v3 v3 v4) (< 397 (div (- i1) 60))) :named IP_137)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) v3 (distinct (- i1) 35)) :named IP_138)) +(assert (! (or v3 (< 397 (div (- i1) 60)) (distinct (- i1) 35)) :named IP_139)) +(assert (! (or (< 397 (div (- i1) 60)) (< 397 (div (- i1) 60)) v3) :named IP_140)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (< 397 (div (- i1) 60)) v0) :named IP_141)) +(assert (! (or (< 397 (div (- i1) 60)) (not v4) v3) :named IP_142)) +(assert (! (or (< 397 (div (- i1) 60)) (distinct v4 (= v0 v4 v3 v3 v4)) (distinct (- i1) 35)) :named IP_143)) +(assert (! (or v3 (is_int 1193124502.0) v3) :named IP_144)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) v0 (< 397 (div (- i1) 60))) :named IP_145)) +(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (not v4) v3) :named IP_146)) +(check-sat-assuming (IP_107 IP_133)) +(get-unsat-core) +(exit) \ No newline at end of file -- cgit v1.2.3 From 75359f120b1cdfa77add48ef11c776f530783c31 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Tue, 1 Dec 2020 16:08:07 +0100 Subject: Add regressions from #5099 (#5557) The issue from #5099 has been fixed in the meantime, this PR adds the examples as regressions. Closes #5099. --- test/regress/CMakeLists.txt | 2 ++ test/regress/regress0/issue5099-model-1.smt2 | 10 ++++++++++ test/regress/regress0/issue5099-model-2.smt2 | 9 +++++++++ 3 files changed, 21 insertions(+) create mode 100644 test/regress/regress0/issue5099-model-1.smt2 create mode 100644 test/regress/regress0/issue5099-model-2.smt2 diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 6c064833a..1a2451147 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -585,6 +585,8 @@ set(regress_0_tests regress0/issue4010-sort-inf-var.smt2 regress0/issue4469-unc-no-reuse-var.smt2 regress0/issue4707-bv-to-bool-small.smt2 + regress0/issue5099-model-1.smt2 + regress0/issue5099-model-2.smt2 regress0/issue5144-resetAssertions.smt2 regress0/ite.cvc regress0/ite2.smt2 diff --git a/test/regress/regress0/issue5099-model-1.smt2 b/test/regress/regress0/issue5099-model-1.smt2 new file mode 100644 index 000000000..dd422ab3b --- /dev/null +++ b/test/regress/regress0/issue5099-model-1.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: -m +; EXPECT: sat +; EXPECT: ((baz true)) +(set-logic QF_NIRA) +(declare-fun a () Int) +(declare-fun b () Int) +(assert (! (or (= a (div 0 b))) :named baz)) +(assert (and (> b 5))) +(check-sat) +(get-assignment) diff --git a/test/regress/regress0/issue5099-model-2.smt2 b/test/regress/regress0/issue5099-model-2.smt2 new file mode 100644 index 000000000..2bd27093f --- /dev/null +++ b/test/regress/regress0/issue5099-model-2.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: -m +; EXPECT: sat +; EXPECT: ((IP true)) +(set-logic QF_NRA) +(declare-const r11 Real) +(declare-const r16 Real) +(assert (! (distinct (/ 1 r16) r11) :named IP)) +(check-sat) +(get-assignment) \ No newline at end of file -- cgit v1.2.3 From 9cbf861d698aaa44d79ca7bd4714064a55f31fba Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Tue, 1 Dec 2020 16:44:32 +0100 Subject: Refactor transcendental solver (#5539) This PR does another round of refactoring on the transcendental solver. It cleans up some variable names, introduces an enum type for Convexity and passes both the intended taylor degree and the actual taylor degree (which will be needed for proofs). --- .../arith/nl/transcendental/exponential_solver.cpp | 26 +++-- .../arith/nl/transcendental/exponential_solver.h | 10 +- src/theory/arith/nl/transcendental/sine_solver.cpp | 21 ++-- src/theory/arith/nl/transcendental/sine_solver.h | 9 +- .../arith/nl/transcendental/taylor_generator.cpp | 4 +- .../arith/nl/transcendental/taylor_generator.h | 10 +- .../nl/transcendental/transcendental_solver.cpp | 8 +- .../nl/transcendental/transcendental_state.cpp | 121 +++++++++++++-------- .../arith/nl/transcendental/transcendental_state.h | 60 +++++++--- 9 files changed, 176 insertions(+), 93 deletions(-) diff --git a/src/theory/arith/nl/transcendental/exponential_solver.cpp b/src/theory/arith/nl/transcendental/exponential_solver.cpp index 7d7d0c23c..482e3bc21 100644 --- a/src/theory/arith/nl/transcendental/exponential_solver.cpp +++ b/src/theory/arith/nl/transcendental/exponential_solver.cpp @@ -170,31 +170,41 @@ void ExponentialSolver::doTangentLemma(TNode e, TNode c, TNode poly_approx) d_data->d_im.addPendingArithLemma(lem, InferenceId::NL_T_TANGENT, nullptr, true); } -void ExponentialSolver::doSecantLemmas( - TNode e, TNode poly_approx, TNode c, TNode poly_approx_c, unsigned d) +void ExponentialSolver::doSecantLemmas(TNode e, + TNode poly_approx, + TNode center, + TNode cval, + unsigned d, + unsigned actual_d) { - d_data->doSecantLemmas( - getSecantBounds(e, c, d), poly_approx, c, poly_approx_c, e, d, 1); + d_data->doSecantLemmas(getSecantBounds(e, center, d), + poly_approx, + center, + cval, + e, + Convexity::CONVEX, + d, + actual_d); } std::pair ExponentialSolver::getSecantBounds(TNode e, - TNode c, + TNode center, unsigned d) { - std::pair bounds = d_data->getClosestSecantPoints(e, c, d); + std::pair bounds = d_data->getClosestSecantPoints(e, center, d); // Check if we already have neighboring secant points if (bounds.first.isNull()) { // pick c-1 bounds.first = Rewriter::rewrite( - NodeManager::currentNM()->mkNode(Kind::MINUS, c, d_data->d_one)); + NodeManager::currentNM()->mkNode(Kind::MINUS, center, d_data->d_one)); } if (bounds.second.isNull()) { // pick c+1 bounds.second = Rewriter::rewrite( - NodeManager::currentNM()->mkNode(Kind::PLUS, c, d_data->d_one)); + NodeManager::currentNM()->mkNode(Kind::PLUS, center, d_data->d_one)); } return bounds; } diff --git a/src/theory/arith/nl/transcendental/exponential_solver.h b/src/theory/arith/nl/transcendental/exponential_solver.h index b20c23e56..b4d08559a 100644 --- a/src/theory/arith/nl/transcendental/exponential_solver.h +++ b/src/theory/arith/nl/transcendental/exponential_solver.h @@ -87,12 +87,16 @@ class ExponentialSolver void doTangentLemma(TNode e, TNode c, TNode poly_approx); /** Sent secant lemmas around c for e */ - void doSecantLemmas( - TNode e, TNode poly_approx, TNode c, TNode poly_approx_c, unsigned d); + void doSecantLemmas(TNode e, + TNode poly_approx, + TNode center, + TNode cval, + unsigned d, + unsigned actual_d); private: /** Generate bounds for secant lemmas */ - std::pair getSecantBounds(TNode e, TNode c, unsigned d); + std::pair getSecantBounds(TNode e, TNode center, unsigned d); /** Holds common state for transcendental solvers */ TranscendentalState* d_data; diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp index 31fd47503..cba85b80e 100644 --- a/src/theory/arith/nl/transcendental/sine_solver.cpp +++ b/src/theory/arith/nl/transcendental/sine_solver.cpp @@ -266,19 +266,20 @@ void SineSolver::doTangentLemma(TNode e, TNode c, TNode poly_approx, int region) // Figure 3: T( x ) // We use zero slope tangent planes, since the concavity of the Taylor // approximation cannot be easily established. - int concavity = regionToConcavity(region); + Convexity convexity = regionToConvexity(region); int mdir = regionToMonotonicityDir(region); + bool usec = (mdir == 1) == (convexity == Convexity::CONCAVE); Node lem = nm->mkNode( Kind::IMPLIES, nm->mkNode( Kind::AND, - nm->mkNode(Kind::GEQ, - e[0], - mdir == concavity ? Node(c) : regionToLowerBound(region)), - nm->mkNode(Kind::LEQ, - e[0], - mdir != concavity ? Node(c) : regionToUpperBound(region))), - nm->mkNode(concavity == 1 ? Kind::GEQ : Kind::LEQ, e, poly_approx)); + nm->mkNode( + Kind::GEQ, e[0], usec ? Node(c) : regionToLowerBound(region)), + nm->mkNode( + Kind::LEQ, e[0], usec ? Node(c) : regionToUpperBound(region))), + nm->mkNode(convexity == Convexity::CONVEX ? Kind::GEQ : Kind::LEQ, + e, + poly_approx)); Trace("nl-ext-sine") << "*** Tangent plane lemma (pre-rewrite): " << lem << std::endl; @@ -294,6 +295,7 @@ void SineSolver::doSecantLemmas(TNode e, TNode c, TNode poly_approx_c, unsigned d, + unsigned actual_d, int region) { d_data->doSecantLemmas(getSecantBounds(e, c, d, region), @@ -301,8 +303,9 @@ void SineSolver::doSecantLemmas(TNode e, c, poly_approx_c, e, + regionToConvexity(region), d, - regionToConcavity(region)); + actual_d); } std::pair SineSolver::getSecantBounds(TNode e, diff --git a/src/theory/arith/nl/transcendental/sine_solver.h b/src/theory/arith/nl/transcendental/sine_solver.h index 9f9102a53..e41e6bd4f 100644 --- a/src/theory/arith/nl/transcendental/sine_solver.h +++ b/src/theory/arith/nl/transcendental/sine_solver.h @@ -93,6 +93,7 @@ class SineSolver TNode c, TNode poly_approx_c, unsigned d, + unsigned actual_d, int region); private: @@ -152,15 +153,15 @@ class SineSolver default: return 0; } } - int regionToConcavity(int region) + Convexity regionToConvexity(int region) { switch (region) { case 1: - case 2: return -1; + case 2: return Convexity::CONCAVE; case 3: - case 4: return 1; - default: return 0; + case 4: return Convexity::CONVEX; + default: return Convexity::UNKNOWN; } } diff --git a/src/theory/arith/nl/transcendental/taylor_generator.cpp b/src/theory/arith/nl/transcendental/taylor_generator.cpp index a373339e9..1b7257f8f 100644 --- a/src/theory/arith/nl/transcendental/taylor_generator.cpp +++ b/src/theory/arith/nl/transcendental/taylor_generator.cpp @@ -212,7 +212,7 @@ void TaylorGenerator::getPolynomialApproximationBounds( } } -void TaylorGenerator::getPolynomialApproximationBoundForArg( +unsigned TaylorGenerator::getPolynomialApproximationBoundForArg( Kind k, Node c, unsigned d, std::vector& pbounds) { getPolynomialApproximationBounds(k, d, pbounds); @@ -252,7 +252,9 @@ void TaylorGenerator::getPolynomialApproximationBoundForArg( getPolynomialApproximationBounds(k, ds, pboundss); pbounds[2] = pboundss[2]; } + return ds; } + return d; } std::pair TaylorGenerator::getTfModelBounds(Node tf, unsigned d, NlModel& model) diff --git a/src/theory/arith/nl/transcendental/taylor_generator.h b/src/theory/arith/nl/transcendental/taylor_generator.h index c647f7fd2..2dbfcccde 100644 --- a/src/theory/arith/nl/transcendental/taylor_generator.h +++ b/src/theory/arith/nl/transcendental/taylor_generator.h @@ -79,11 +79,13 @@ class TaylorGenerator * polynomials may depend on c. In particular, for P_u+[x] for ( c ) where * c>0, we return the P_u+[x] from the function above for the minimum degree * d' >= d such that (1-c^{2*d'+1}/(2*d'+1)!) is positive. + * @return the actual degree of the polynomial approximations (which may be + * larger than d). */ - void getPolynomialApproximationBoundForArg(Kind k, - Node c, - unsigned d, - std::vector& pbounds); + unsigned getPolynomialApproximationBoundForArg(Kind k, + Node c, + unsigned d, + std::vector& pbounds); /** get transcendental function model bounds * diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp index 8eb69e50b..ad3f49576 100644 --- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp @@ -233,7 +233,8 @@ bool TranscendentalSolver::checkTfTangentPlanesFun(Node tf, unsigned d) // mapped to for signs of c std::map poly_approx_bounds[2]; std::vector pbounds; - d_tstate.d_taylor.getPolynomialApproximationBoundForArg(k, c, d, pbounds); + unsigned actual_d = + d_tstate.d_taylor.getPolynomialApproximationBoundForArg(k, c, d, pbounds); poly_approx_bounds[0][1] = pbounds[0]; poly_approx_bounds[0][-1] = pbounds[1]; poly_approx_bounds[1][1] = pbounds[2]; @@ -362,11 +363,12 @@ bool TranscendentalSolver::checkTfTangentPlanesFun(Node tf, unsigned d) { if (k == EXPONENTIAL) { - d_expSlv.doSecantLemmas(tf, poly_approx, c, poly_approx_c, d); + d_expSlv.doSecantLemmas(tf, poly_approx, c, poly_approx_c, d, actual_d); } else if (k == Kind::SINE) { - d_sineSlv.doSecantLemmas(tf, poly_approx, c, poly_approx_c, d, region); + d_sineSlv.doSecantLemmas( + tf, poly_approx, c, poly_approx_c, d, actual_d, region); } } return true; diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp index 41ed2c53d..69678c621 100644 --- a/src/theory/arith/nl/transcendental/transcendental_state.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp @@ -267,26 +267,26 @@ void TranscendentalState::getCurrentPiBounds() } std::pair TranscendentalState::getClosestSecantPoints(TNode e, - TNode c, + TNode center, unsigned d) { // bounds are the minimum and maximum previous secant points // should not repeat secant points: secant lemmas should suffice to // rule out previous assignment - Assert( - std::find(d_secant_points[e][d].begin(), d_secant_points[e][d].end(), c) - == d_secant_points[e][d].end()); + Assert(std::find( + d_secant_points[e][d].begin(), d_secant_points[e][d].end(), center) + == d_secant_points[e][d].end()); // Insert into the (temporary) vector. We do not update this vector // until we are sure this secant plane lemma has been processed. We do // this by mapping the lemma to a side effect below. std::vector spoints = d_secant_points[e][d]; - spoints.push_back(c); + spoints.push_back(center); // sort sortByNlModel(spoints.begin(), spoints.end(), &d_model); // get the resulting index of c unsigned index = - std::find(spoints.begin(), spoints.end(), c) - spoints.begin(); + std::find(spoints.begin(), spoints.end(), center) - spoints.begin(); // bounds are the next closest upper/lower bound values return {index > 0 ? spoints[index - 1] : Node(), @@ -294,24 +294,40 @@ std::pair TranscendentalState::getClosestSecantPoints(TNode e, } Node TranscendentalState::mkSecantPlane( - TNode arg, TNode b, TNode c, TNode approx_b, TNode approx_c) + TNode arg, TNode lower, TNode upper, TNode lval, TNode uval) { NodeManager* nm = NodeManager::currentNM(); // Figure 3: S_l( x ), S_u( x ) for s = 0,1 - Node rcoeff_n = Rewriter::rewrite(nm->mkNode(Kind::MINUS, b, c)); + Node rcoeff_n = Rewriter::rewrite(nm->mkNode(Kind::MINUS, lower, upper)); Assert(rcoeff_n.isConst()); Rational rcoeff = rcoeff_n.getConst(); Assert(rcoeff.sgn() != 0); - return nm->mkNode(Kind::PLUS, - approx_b, - nm->mkNode(Kind::MULT, - nm->mkNode(Kind::MINUS, approx_b, approx_c), - nm->mkConst(rcoeff.inverse()), - nm->mkNode(Kind::MINUS, arg, b))); + Node res = + nm->mkNode(Kind::PLUS, + lval, + nm->mkNode(Kind::MULT, + nm->mkNode(Kind::DIVISION, + nm->mkNode(Kind::MINUS, lval, uval), + nm->mkNode(Kind::MINUS, lower, upper)), + nm->mkNode(Kind::MINUS, arg, lower))); + Trace("nl-trans") << "Creating secant plane for transcendental function of " + << arg << std::endl; + Trace("nl-trans") << "\tfrom ( " << lower << " ; " << lval << " ) to ( " + << upper << " ; " << uval << " )" << std::endl; + Trace("nl-trans") << "\t" << res << std::endl; + Trace("nl-trans") << "\trewritten: " << Rewriter::rewrite(res) << std::endl; + return res; } -NlLemma TranscendentalState::mkSecantLemma( - TNode lower, TNode upper, int concavity, TNode tf, TNode splane) +NlLemma TranscendentalState::mkSecantLemma(TNode lower, + TNode upper, + TNode lapprox, + TNode uapprox, + int csign, + Convexity convexity, + TNode tf, + TNode splane, + unsigned actual_d) { NodeManager* nm = NodeManager::currentNM(); // With respect to Figure 3, this is slightly different. @@ -329,60 +345,73 @@ NlLemma TranscendentalState::mkSecantLemma( Node antec_n = nm->mkNode(Kind::AND, nm->mkNode(Kind::GEQ, tf[0], lower), nm->mkNode(Kind::LEQ, tf[0], upper)); + Trace("nl-trans") << "Bound for secant plane: " << lower << " <= " << tf[0] + << " <= " << upper << std::endl; + Trace("nl-trans") << "\t" << antec_n << std::endl; + // Convex: actual value is below the secant + // Concave: actual value is above the secant Node lem = nm->mkNode( Kind::IMPLIES, antec_n, - nm->mkNode(concavity == 1 ? Kind::LEQ : Kind::GEQ, tf, splane)); - Trace("nl-ext-tftp-debug2") - << "*** Secant plane lemma (pre-rewrite) : " << lem << std::endl; + nm->mkNode( + convexity == Convexity::CONVEX ? Kind::LEQ : Kind::GEQ, tf, splane)); + Trace("nl-trans-lemma") << "*** Secant plane lemma (pre-rewrite) : " << lem + << std::endl; lem = Rewriter::rewrite(lem); - Trace("nl-ext-tftp-lemma") << "*** Secant plane lemma : " << lem << std::endl; + Trace("nl-trans-lemma") << "*** Secant plane lemma : " << lem << std::endl; Assert(d_model.computeAbstractModelValue(lem) == d_false); return NlLemma(lem, LemmaProperty::NONE, nullptr, InferenceId::NL_T_SECANT); } void TranscendentalState::doSecantLemmas(const std::pair& bounds, TNode poly_approx, - TNode c, - TNode approx_c, + TNode center, + TNode cval, TNode tf, + Convexity convexity, unsigned d, - int concavity) + unsigned actual_d) { - Trace("nl-ext-tftp-debug2") << "...secant bounds are : " << bounds.first - << " ... " << bounds.second << std::endl; - // take the model value of l or u (since may contain PI) - // Make secant from bounds.first to c - Node lval = d_model.computeAbstractModelValue(bounds.first); - Trace("nl-ext-tftp-debug2") << "...model value of bound " << bounds.first - << " is " << lval << std::endl; - if (lval != c) + int csign = center.getConst().sgn(); + Trace("nl-trans") << "...do secant lemma with center " << center << " val " + << cval << " sign " << csign << std::endl; + Trace("nl-trans") << "...secant bounds are : " << bounds.first << " ... " + << bounds.second << std::endl; + // take the model value of lower (since may contain PI) + // Make secant from bounds.first to center + Node lower = d_model.computeAbstractModelValue(bounds.first); + Trace("nl-trans") << "...model value of bound " << bounds.first << " is " + << lower << std::endl; + if (lower != center) { // Figure 3 : P(l), P(u), for s = 0 - Node approx_l = Rewriter::rewrite( - poly_approx.substitute(d_taylor.getTaylorVariable(), lval)); - Node splane = mkSecantPlane(tf[0], lval, c, approx_l, approx_c); - NlLemma nlem = mkSecantLemma(lval, c, concavity, tf, splane); + Node lval = Rewriter::rewrite( + poly_approx.substitute(d_taylor.getTaylorVariable(), lower)); + Node splane = mkSecantPlane(tf[0], lower, center, lval, cval); + NlLemma nlem = mkSecantLemma( + lower, center, lval, cval, csign, convexity, tf, splane, actual_d); // The side effect says that if lem is added, then we should add the // secant point c for (tf,d). - nlem.d_secantPoint.push_back(std::make_tuple(tf, d, c)); + nlem.d_secantPoint.push_back(std::make_tuple(tf, d, center)); d_im.addPendingArithLemma(nlem, true); } - // Make secant from c to bounds.second - Node uval = d_model.computeAbstractModelValue(bounds.second); - Trace("nl-ext-tftp-debug2") << "...model value of bound " << bounds.second - << " is " << uval << std::endl; - if (c != uval) + // take the model value of upper (since may contain PI) + // Make secant from center to bounds.second + Node upper = d_model.computeAbstractModelValue(bounds.second); + Trace("nl-trans") << "...model value of bound " << bounds.second << " is " + << upper << std::endl; + if (center != upper) { // Figure 3 : P(l), P(u), for s = 1 - Node approx_u = Rewriter::rewrite( - poly_approx.substitute(d_taylor.getTaylorVariable(), uval)); - Node splane = mkSecantPlane(tf[0], c, uval, approx_c, approx_u); - NlLemma nlem = mkSecantLemma(c, uval, concavity, tf, splane); + Node uval = Rewriter::rewrite( + poly_approx.substitute(d_taylor.getTaylorVariable(), upper)); + Node splane = mkSecantPlane(tf[0], center, upper, cval, uval); + NlLemma nlem = mkSecantLemma( + center, upper, cval, uval, csign, convexity, tf, splane, actual_d); // The side effect says that if lem is added, then we should add the // secant point c for (tf,d). - nlem.d_secantPoint.push_back(std::make_tuple(tf, d, c)); + nlem.d_secantPoint.push_back(std::make_tuple(tf, d, center)); d_im.addPendingArithLemma(nlem, true); } } diff --git a/src/theory/arith/nl/transcendental/transcendental_state.h b/src/theory/arith/nl/transcendental/transcendental_state.h index 0a4e46eca..e1510c3b3 100644 --- a/src/theory/arith/nl/transcendental/transcendental_state.h +++ b/src/theory/arith/nl/transcendental/transcendental_state.h @@ -26,6 +26,24 @@ namespace arith { namespace nl { namespace transcendental { +/** + * This enum indicates whether some function is convex, concave or unknown at + * some point. + */ +enum class Convexity +{ + CONVEX, + CONCAVE, + UNKNOWN +}; +inline std::ostream& operator<<(std::ostream& os, Convexity c) { + switch (c) { + case Convexity::CONVEX: return os << "CONVEX"; + case Convexity::CONCAVE: return os << "CONCAVE"; + default: return os << "UNKNOWN"; + } +} + /** * Holds common state and utilities for transcendental solvers. * @@ -60,20 +78,24 @@ struct TranscendentalState * Get the two closest secant points from the once stored already. * "closest" is determined according to the current model. * @param e The transcendental term (like (exp t)) - * @param c The point currently under consideration (probably the model of t) + * @param center The point currently under consideration (probably the model + * of t) * @param d The taylor degree. */ - std::pair getClosestSecantPoints(TNode e, TNode c, unsigned d); + std::pair getClosestSecantPoints(TNode e, + TNode center, + unsigned d); /** - * Construct a secant plane between b and c + * Construct a secant plane as function in arg between lower and upper * @param arg The argument of the transcendental term - * @param b Left secant point - * @param c Right secant point - * @param approx Approximation for b (not yet substituted) - * @param approx_c Approximation for c (already substituted) + * @param lower Left secant point + * @param upper Right secant point + * @param lval Evaluation at lower + * @param uval Evaluation at upper */ - Node mkSecantPlane(TNode arg, TNode b, TNode c, TNode approx, TNode approx_c); + Node mkSecantPlane( + TNode arg, TNode lower, TNode upper, TNode lval, TNode uval); /** * Construct a secant lemma between lower and upper for tf. @@ -83,26 +105,34 @@ struct TranscendentalState * @param tf Current transcendental term * @param splane Secant plane as computed by mkSecantPlane() */ - NlLemma mkSecantLemma( - TNode lower, TNode upper, int concavity, TNode tf, TNode splane); + NlLemma mkSecantLemma(TNode lower, + TNode upper, + TNode lapprox, + TNode uapprox, + int csign, + Convexity convexity, + TNode tf, + TNode splane, + unsigned actual_d); /** * Construct and send secant lemmas (if appropriate) * @param bounds Secant bounds * @param poly_approx Polynomial approximation - * @param c Current point - * @param approx_c Approximation for c + * @param center Current point + * @param cval Evaluation at c * @param tf Current transcendental term * @param d Current taylor degree * @param concavity Concavity in region of c */ void doSecantLemmas(const std::pair& bounds, TNode poly_approx, - TNode c, - TNode approx_c, + TNode center, + TNode cval, TNode tf, + Convexity convexity, unsigned d, - int concavity); + unsigned actual_d); Node d_true; Node d_false; -- cgit v1.2.3 From 41554fa3d4a8258bbc842aedad87cd218460ee0a Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 1 Dec 2020 08:58:06 -0800 Subject: Improve rewriting of str.<= (#4848) This commit improves our rewriting of str.<= slightly. If we have constant prefixes that are different, we can always rewrite the term to a constant. Previously, we were only doing so when the result was false. --- src/theory/strings/strings_rewriter.cpp | 14 +++-- test/regress/CMakeLists.txt | 1 + test/regress/regress0/strings/leq.smt2 | 10 ++++ test/unit/theory/CMakeLists.txt | 1 + test/unit/theory/strings_rewriter_white.h | 89 +++++++++++++++++++++++++++++++ 5 files changed, 107 insertions(+), 8 deletions(-) create mode 100644 test/regress/regress0/strings/leq.smt2 create mode 100644 test/unit/theory/strings_rewriter_white.h diff --git a/src/theory/strings/strings_rewriter.cpp b/src/theory/strings/strings_rewriter.cpp index 932b5c8cc..575c33501 100644 --- a/src/theory/strings/strings_rewriter.cpp +++ b/src/theory/strings/strings_rewriter.cpp @@ -251,15 +251,13 @@ Node StringsRewriter::rewriteStringLeq(Node n) { String s = n1[0].getConst(); String t = n2[0].getConst(); - // only need to truncate if s is longer - if (s.size() > t.size()) + size_t prefixLen = std::min(s.size(), t.size()); + s = s.prefix(prefixLen); + t = t.prefix(prefixLen); + // if the prefixes are not the same, then we can already decide the outcome + if (s != t) { - s = s.prefix(t.size()); - } - // if prefix is not leq, then entire string is not leq - if (!s.isLeq(t)) - { - Node ret = nm->mkConst(false); + Node ret = nm->mkConst(s.isLeq(t)); return returnRewrite(n, ret, Rewrite::STR_LEQ_CPREFIX); } } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 1a2451147..fb8914a36 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1019,6 +1019,7 @@ set(regress_0_tests regress0/strings/itos-entail.smt2 regress0/strings/large-model.smt2 regress0/strings/leadingzero001.smt2 + regress0/strings/leq.smt2 regress0/strings/loop001.smt2 regress0/strings/loop-wrong-sem.smt2 regress0/strings/model001.smt2 diff --git a/test/regress/regress0/strings/leq.smt2 b/test/regress/regress0/strings/leq.smt2 new file mode 100644 index 000000000..b3bd40739 --- /dev/null +++ b/test/regress/regress0/strings/leq.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --strings-exp +(set-logic QF_SLIA) +(declare-const x String) +(declare-const y String) +(assert (or + (not (str.<= (str.++ "A" x) (str.++ "B" y))) + (not (str.<= (str.++ "A" x) (str.++ "BC" y))) + (str.<= (str.++ "A" "D" x) (str.++ "AC" y)))) +(set-info :status unsat) +(check-sat) diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt index 8cfd43989..0eccbf436 100644 --- a/test/unit/theory/CMakeLists.txt +++ b/test/unit/theory/CMakeLists.txt @@ -13,6 +13,7 @@ cvc4_add_unit_test_black(theory_black theory) cvc4_add_unit_test_white(evaluator_white theory) cvc4_add_unit_test_white(logic_info_white theory) cvc4_add_unit_test_white(sequences_rewriter_white theory) +cvc4_add_unit_test_white(strings_rewriter_white theory) cvc4_add_unit_test_white(theory_arith_white theory) cvc4_add_unit_test_white(theory_bags_normal_form_white theory) cvc4_add_unit_test_white(theory_bags_rewriter_white theory) diff --git a/test/unit/theory/strings_rewriter_white.h b/test/unit/theory/strings_rewriter_white.h new file mode 100644 index 000000000..f5c7cced8 --- /dev/null +++ b/test/unit/theory/strings_rewriter_white.h @@ -0,0 +1,89 @@ +/********************* */ +/*! \file strings_rewriter_white.h + ** \verbatim + ** Top contributors (to current version): + ** Andres Noetzli + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 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 Unit tests for the strings rewriter + ** + ** Unit tests for the strings rewriter. + **/ + +#include + +#include +#include +#include + +#include "expr/node.h" +#include "expr/node_manager.h" +#include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" +#include "theory/rewriter.h" +#include "theory/strings/strings_rewriter.h" + +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::smt; +using namespace CVC4::theory; +using namespace CVC4::theory::strings; + +class StringsRewriterWhite : public CxxTest::TestSuite +{ + public: + StringsRewriterWhite() {} + + void setUp() override + { + Options opts; + opts.setOutputLanguage(language::output::LANG_SMTLIB_V2); + d_em = new ExprManager; + d_nm = NodeManager::fromExprManager(d_em); + d_smt = new SmtEngine(d_nm, &opts); + d_scope = new SmtScope(d_smt); + d_smt->finishInit(); + } + + void tearDown() override + { + delete d_scope; + delete d_smt; + delete d_em; + } + + void testRewriteLeq() + { + TypeNode intType = d_nm->integerType(); + TypeNode strType = d_nm->stringType(); + + Node a = d_nm->mkConst(::CVC4::String("A")); + Node bc = d_nm->mkConst(::CVC4::String("BC")); + Node x = d_nm->mkVar("x", strType); + Node y = d_nm->mkVar("y", strType); + + Node ax = d_nm->mkNode(STRING_CONCAT, a, x); + Node bcy = d_nm->mkNode(STRING_CONCAT, bc, y); + + { + Node leq = d_nm->mkNode(STRING_LEQ, ax, bcy); + TS_ASSERT_EQUALS(Rewriter::rewrite(leq), d_nm->mkConst(true)); + } + + { + Node leq = d_nm->mkNode(STRING_LEQ, bcy, ax); + TS_ASSERT_EQUALS(Rewriter::rewrite(leq), d_nm->mkConst(false)); + } + } + + private: + ExprManager* d_em; + SmtEngine* d_smt; + SmtScope* d_scope; + + NodeManager* d_nm; +}; -- cgit v1.2.3 From 798644e64f438f320577a444110744041e39d1ff Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 1 Dec 2020 18:00:49 -0600 Subject: Fix issues related to model declarations (#5560) This corrects two issues related to model declarations: (1) model declaration terms were mistaken not cleared, (2) the model needs to be explicitly destructed before the node manager because it contains references to Node. Fixes #5540 --- src/smt/model.cpp | 6 +++++- src/smt/smt_engine.cpp | 1 + test/regress/CMakeLists.txt | 2 ++ test/regress/regress0/issue5540-2-dump-model.smt2 | 9 +++++++++ test/regress/regress0/issue5540-model-decls.smt2 | 19 +++++++++++++++++++ 5 files changed, 36 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress0/issue5540-2-dump-model.smt2 create mode 100644 test/regress/regress0/issue5540-model-decls.smt2 diff --git a/src/smt/model.cpp b/src/smt/model.cpp index 8a9f944d2..ccf73dda0 100644 --- a/src/smt/model.cpp +++ b/src/smt/model.cpp @@ -49,7 +49,11 @@ Node Model::getValue(TNode n) const { return d_tmodel->getValue(n); } bool Model::hasApproximations() const { return d_tmodel->hasApproximations(); } -void Model::clearModelDeclarations() { d_declareSorts.clear(); } +void Model::clearModelDeclarations() +{ + d_declareTerms.clear(); + d_declareSorts.clear(); +} void Model::addDeclarationSort(TypeNode tn) { d_declareSorts.push_back(tn); } diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index d3ba676fc..2faad7961 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -332,6 +332,7 @@ SmtEngine::~SmtEngine() d_absValues.reset(nullptr); d_asserts.reset(nullptr); d_dumpm.reset(nullptr); + d_model.reset(nullptr); d_sygusSolver.reset(nullptr); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index fb8914a36..fda5c69eb 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -588,6 +588,8 @@ set(regress_0_tests regress0/issue5099-model-1.smt2 regress0/issue5099-model-2.smt2 regress0/issue5144-resetAssertions.smt2 + regress0/issue5540-2-dump-model.smt2 + regress0/issue5540-model-decls.smt2 regress0/ite.cvc regress0/ite2.smt2 regress0/ite3.smt2 diff --git a/test/regress/regress0/issue5540-2-dump-model.smt2 b/test/regress/regress0/issue5540-2-dump-model.smt2 new file mode 100644 index 000000000..56d3b2458 --- /dev/null +++ b/test/regress/regress0/issue5540-2-dump-model.smt2 @@ -0,0 +1,9 @@ +; SCRUBBER: sed -e 's/Bool.*$/Bool/' +; COMMAND-LINE: --dump-models +; EXPECT: sat +; EXPECT: ( +; EXPECT: (define-fun v16 () Bool +; EXPECT: ) +(set-logic UFLIA) +(declare-fun v16 () Bool) +(check-sat) diff --git a/test/regress/regress0/issue5540-model-decls.smt2 b/test/regress/regress0/issue5540-model-decls.smt2 new file mode 100644 index 000000000..714159c9f --- /dev/null +++ b/test/regress/regress0/issue5540-model-decls.smt2 @@ -0,0 +1,19 @@ +; SCRUBBER: sed -e 's/Bool.*$/Bool/' +; COMMAND-LINE: --dump-models -i +; EXPECT:sat +; EXPECT: ( +; EXPECT: (define-fun a () Bool +; EXPECT: ) +; EXPECT: sat +; EXPECT: ( +; EXPECT: (define-fun a () Bool +; EXPECT: ) +; EXPECT: sat +; EXPECT: ( +; EXPECT: (define-fun a () Bool +; EXPECT: ) +(set-logic ALL) +(declare-fun a () Bool) +(check-sat) +(check-sat) +(check-sat) -- cgit v1.2.3 From a87df2bb60a8739d4eb24b60efca79f8d2b7d806 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Tue, 1 Dec 2020 16:30:33 -0800 Subject: google test: Infrastructure and first api test. (#5548) This sets up the infrastructure for migrating unit tests from CxxTest to Google Test. It further migrates api/datatype_api_black to the new infrastructure. --- .github/workflows/ci.yml | 6 + CMakeLists.txt | 2 +- INSTALL.md | 8 +- test/unit/CMakeLists.txt | 51 ++- test/unit/api/CMakeLists.txt | 12 +- test/unit/api/datatype_api_black.cpp | 540 +++++++++++++++++++++++++++++++ test/unit/api/datatype_api_black.h | 576 --------------------------------- test/unit/base/CMakeLists.txt | 2 +- test/unit/context/CMakeLists.txt | 14 +- test/unit/expr/CMakeLists.txt | 34 +- test/unit/main/CMakeLists.txt | 2 +- test/unit/parser/CMakeLists.txt | 4 +- test/unit/preprocessing/CMakeLists.txt | 2 +- test/unit/printer/CMakeLists.txt | 2 +- test/unit/prop/CMakeLists.txt | 2 +- test/unit/test_api.h | 27 ++ test/unit/theory/CMakeLists.txt | 42 +-- test/unit/util/CMakeLists.txt | 36 +-- 18 files changed, 707 insertions(+), 655 deletions(-) create mode 100644 test/unit/api/datatype_api_black.cpp delete mode 100644 test/unit/api/datatype_api_black.h create mode 100644 test/unit/test_api.h diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index acc13c2ee..5da6b4208 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -61,10 +61,12 @@ jobs: run: | sudo apt-get update sudo apt-get install -y \ + build-essential \ ccache \ cxxtest \ libcln-dev \ libgmp-dev \ + libgtest-dev \ libedit-dev \ flex \ libfl-dev \ @@ -72,6 +74,10 @@ jobs: python3 -m pip install toml python3 -m pip install setuptools python3 -m pip install pexpect + cd /usr/src/googletest + sudo cmake . + sudo cmake --build . --target install + cd - echo "/usr/lib/ccache" >> $GITHUB_PATH # Note: macOS comes with a libedit; it does not need to brew-installed diff --git a/CMakeLists.txt b/CMakeLists.txt index 8eab22e4a..6c3ed4bbc 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -8,7 +8,7 @@ ## All rights reserved. See the file COPYING in the top-level source ## directory for licensing information. ## -cmake_minimum_required(VERSION 3.4) +cmake_minimum_required(VERSION 3.9) #-----------------------------------------------------------------------------# # Project configuration diff --git a/INSTALL.md b/INSTALL.md index b3308726b..5693dbc1c 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -46,7 +46,7 @@ compatible. - [GNU C and C++ (gcc and g++)](https://gcc.gnu.org) or [Clang](https://clang.llvm.org) (reasonably recent versions) -- [CMake >= 3.1](https://cmake.org) +- [CMake >= 3.9](https://cmake.org) - [GNU Bash](https://www.gnu.org/software/bash/) - [Python >= 2.7](https://www.python.org) + module [toml](https://pypi.org/project/toml/) @@ -195,6 +195,12 @@ provided with CVC4. See [Testing CVC4](#Testing-CVC4) below for more details. +### Google Test Unit Testing Framework (Unit Tests) + +[Google Test](https://github.com/google/googletest) is required to optionally +run CVC4's unit tests (included with the distribution). +See [Testing CVC4](#Testing-CVC4) below for more details. + ## Language bindings CVC4 provides a complete and flexible C++ API (see `examples/api` for diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt index bb53c15b0..d65e022c9 100644 --- a/test/unit/CMakeLists.txt +++ b/test/unit/CMakeLists.txt @@ -13,6 +13,8 @@ # custom finder modules). set(CxxTest_HOME ${CXXTEST_DIR}) find_package(CxxTest REQUIRED) +find_package(GTest REQUIRED) +include(GoogleTest) include_directories(.) include_directories(${PROJECT_SOURCE_DIR}/src) @@ -35,10 +37,48 @@ set(CVC4_CXXTEST_FLAGS_BLACK -D__STDC_LIMIT_MACROS -D__STDC_FORMAT_MACROS) set(CVC4_CXXTEST_FLAGS_WHITE -fno-access-control ${CVC4_CXXTEST_FLAGS_BLACK}) +# Generate and add unit test. +macro(cvc4_add_unit_test is_white name output_dir) + set(test_src ${CMAKE_CURRENT_LIST_DIR}/${name}.cpp) + add_executable(${name} ${test_src}) + gtest_add_tests(TARGET ${name}) + target_link_libraries(${name} main-test) + target_link_libraries(${name} GTest::GTest) + target_link_libraries(${name} GTest::Main) + if(USE_LFSC) + # We don't link against LFSC, because CVC4 is already linked against it. + target_include_directories(${name} PRIVATE ${LFSC_INCLUDE_DIR}) + endif() + if(USE_POLY) + # We don't link against libpoly, because CVC4 is already linked against it. + target_include_directories(${name} PRIVATE ${POLY_INCLUDE_DIR}) + endif() + if(${is_white}) + target_compile_options(${name} PRIVATE -fno-access-control) + endif() + add_dependencies(build-units ${name}) + # Generate into bin/test/unit/. + set(test_bin_dir ${CMAKE_BINARY_DIR}/bin/test/unit/${output_dir}) + set_target_properties(${name} + PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${test_bin_dir}) + # The test target is prefixed with test identifier 'unit/' and the path, + # e.g., for '/myunittest.h' + # we create test target 'unit//myunittest' + # and run it with 'ctest -R "example//myunittest"'. + if("${output_dir}" STREQUAL "") + set(test_name unit/${name}) + else() + set(test_name unit/${output_dir}/${name}) + endif() + add_test(${test_name} ${test_bin_dir}/${name}) + set_tests_properties(${test_name} PROPERTIES LABELS "unit") +endmacro() + # Generate and add unit test. # Note: we do not use cxxtest_add_test from the FindCxxTest module since it # does not allow test names containing '/'. -macro(cvc4_add_unit_test is_white name output_dir) +# !! This macro will be removed when all unit tests are migrated to Google Test. +macro(cvc4_add_cxx_unit_test is_white name output_dir) # generate the test sources set(test_src ${CMAKE_CURRENT_BINARY_DIR}/${name}.cpp) set(test_header ${CMAKE_CURRENT_LIST_DIR}/${name}.h) @@ -110,6 +150,15 @@ macro(cvc4_add_unit_test_white name output_dir) cvc4_add_unit_test(TRUE ${name} ${output_dir}) endmacro() +# !! Will be removed when all unit tests are migrated to Google Test. +macro(cvc4_add_cxx_unit_test_black name output_dir) + cvc4_add_cxx_unit_test(FALSE ${name} ${output_dir}) +endmacro() +# !! Will be removed when all unit tests are migrated to Google Test. +macro(cvc4_add_cxx_unit_test_white name output_dir) + cvc4_add_cxx_unit_test(TRUE ${name} ${output_dir}) +endmacro() + add_subdirectory(api) add_subdirectory(base) add_subdirectory(context) diff --git a/test/unit/api/CMakeLists.txt b/test/unit/api/CMakeLists.txt index 1412c7f66..9fcf881a8 100644 --- a/test/unit/api/CMakeLists.txt +++ b/test/unit/api/CMakeLists.txt @@ -12,10 +12,10 @@ # Add unit tests cvc4_add_unit_test_black(datatype_api_black api) -cvc4_add_unit_test_black(op_black api) -cvc4_add_unit_test_black(result_black api) -cvc4_add_unit_test_black(solver_black api) -cvc4_add_unit_test_black(sort_black api) -cvc4_add_unit_test_black(term_black api) -cvc4_add_unit_test_black(grammar_black api) +cvc4_add_cxx_unit_test_black(op_black api) +cvc4_add_cxx_unit_test_black(result_black api) +cvc4_add_cxx_unit_test_black(solver_black api) +cvc4_add_cxx_unit_test_black(sort_black api) +cvc4_add_cxx_unit_test_black(term_black api) +cvc4_add_cxx_unit_test_black(grammar_black api) diff --git a/test/unit/api/datatype_api_black.cpp b/test/unit/api/datatype_api_black.cpp new file mode 100644 index 000000000..f61637221 --- /dev/null +++ b/test/unit/api/datatype_api_black.cpp @@ -0,0 +1,540 @@ +/********************* */ +/*! \file datatype_api_black.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Aina Niemetz, Andres Noetzli + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 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 Black box testing of the datatype classes of the C++ API. + ** + ** Black box testing of the datatype classes of the C++ API. + **/ + +#include "test_api.h" + +using namespace CVC4::api; + +TEST_F(TestApi, mkDatatypeSort) +{ + DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); + DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); + cons.addSelector("head", d_solver.getIntegerSort()); + dtypeSpec.addConstructor(cons); + DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); + dtypeSpec.addConstructor(nil); + Sort listSort = d_solver.mkDatatypeSort(dtypeSpec); + Datatype d = listSort.getDatatype(); + DatatypeConstructor consConstr = d[0]; + DatatypeConstructor nilConstr = d[1]; + EXPECT_THROW(d[2], CVC4ApiException); + ASSERT_NO_THROW(consConstr.getConstructorTerm()); + ASSERT_NO_THROW(nilConstr.getConstructorTerm()); +} + +TEST_F(TestApi, mkDatatypeSorts) +{ + /* Create two mutual datatypes corresponding to this definition + * block: + * + * DATATYPE + * tree = node(left: tree, right: tree) | leaf(data: list), + * list = cons(car: tree, cdr: list) | nil + * END; + */ + // Make unresolved types as placeholders + std::set unresTypes; + Sort unresTree = d_solver.mkUninterpretedSort("tree"); + Sort unresList = d_solver.mkUninterpretedSort("list"); + unresTypes.insert(unresTree); + unresTypes.insert(unresList); + + DatatypeDecl tree = d_solver.mkDatatypeDecl("tree"); + DatatypeConstructorDecl node = d_solver.mkDatatypeConstructorDecl("node"); + node.addSelector("left", unresTree); + node.addSelector("right", unresTree); + tree.addConstructor(node); + + DatatypeConstructorDecl leaf = d_solver.mkDatatypeConstructorDecl("leaf"); + leaf.addSelector("data", unresList); + tree.addConstructor(leaf); + + DatatypeDecl list = d_solver.mkDatatypeDecl("list"); + DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); + cons.addSelector("car", unresTree); + cons.addSelector("cdr", unresTree); + list.addConstructor(cons); + + DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); + list.addConstructor(nil); + + std::vector dtdecls; + dtdecls.push_back(tree); + dtdecls.push_back(list); + std::vector dtsorts; + ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes)); + ASSERT_EQ(dtsorts.size(), dtdecls.size()); + for (size_t i = 0, ndecl = dtdecls.size(); i < ndecl; i++) + { + ASSERT_TRUE(dtsorts[i].isDatatype()); + EXPECT_FALSE(dtsorts[i].getDatatype().isFinite()); + EXPECT_EQ(dtsorts[i].getDatatype().getName(), dtdecls[i].getName()); + } + // verify the resolution was correct + Datatype dtTree = dtsorts[0].getDatatype(); + DatatypeConstructor dtcTreeNode = dtTree[0]; + EXPECT_EQ(dtcTreeNode.getName(), "node"); + DatatypeSelector dtsTreeNodeLeft = dtcTreeNode[0]; + EXPECT_EQ(dtsTreeNodeLeft.getName(), "left"); + // argument type should have resolved to be recursive + EXPECT_TRUE(dtsTreeNodeLeft.getRangeSort().isDatatype()); + EXPECT_EQ(dtsTreeNodeLeft.getRangeSort(), dtsorts[0]); + + // fails due to empty datatype + std::vector dtdeclsBad; + DatatypeDecl emptyD = d_solver.mkDatatypeDecl("emptyD"); + dtdeclsBad.push_back(emptyD); + EXPECT_THROW(d_solver.mkDatatypeSorts(dtdeclsBad), CVC4ApiException); +} + +TEST_F(TestApi, datatypeStructs) +{ + Sort intSort = d_solver.getIntegerSort(); + Sort boolSort = d_solver.getBooleanSort(); + + // create datatype sort to test + DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); + DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); + cons.addSelector("head", intSort); + cons.addSelectorSelf("tail"); + Sort nullSort; + EXPECT_THROW(cons.addSelector("null", nullSort), CVC4ApiException); + dtypeSpec.addConstructor(cons); + DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); + dtypeSpec.addConstructor(nil); + Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); + Datatype dt = dtypeSort.getDatatype(); + EXPECT_FALSE(dt.isCodatatype()); + EXPECT_FALSE(dt.isTuple()); + EXPECT_FALSE(dt.isRecord()); + EXPECT_FALSE(dt.isFinite()); + EXPECT_TRUE(dt.isWellFounded()); + // get constructor + DatatypeConstructor dcons = dt[0]; + Term consTerm = dcons.getConstructorTerm(); + EXPECT_EQ(dcons.getNumSelectors(), 2); + + // create datatype sort to test + DatatypeDecl dtypeSpecEnum = d_solver.mkDatatypeDecl("enum"); + DatatypeConstructorDecl ca = d_solver.mkDatatypeConstructorDecl("A"); + dtypeSpecEnum.addConstructor(ca); + DatatypeConstructorDecl cb = d_solver.mkDatatypeConstructorDecl("B"); + dtypeSpecEnum.addConstructor(cb); + DatatypeConstructorDecl cc = d_solver.mkDatatypeConstructorDecl("C"); + dtypeSpecEnum.addConstructor(cc); + Sort dtypeSortEnum = d_solver.mkDatatypeSort(dtypeSpecEnum); + Datatype dtEnum = dtypeSortEnum.getDatatype(); + EXPECT_FALSE(dtEnum.isTuple()); + EXPECT_TRUE(dtEnum.isFinite()); + + // create codatatype + DatatypeDecl dtypeSpecStream = d_solver.mkDatatypeDecl("stream", true); + DatatypeConstructorDecl consStream = + d_solver.mkDatatypeConstructorDecl("cons"); + consStream.addSelector("head", intSort); + consStream.addSelectorSelf("tail"); + dtypeSpecStream.addConstructor(consStream); + Sort dtypeSortStream = d_solver.mkDatatypeSort(dtypeSpecStream); + Datatype dtStream = dtypeSortStream.getDatatype(); + EXPECT_TRUE(dtStream.isCodatatype()); + EXPECT_FALSE(dtStream.isFinite()); + // codatatypes may be well-founded + EXPECT_TRUE(dtStream.isWellFounded()); + + // create tuple + Sort tupSort = d_solver.mkTupleSort({boolSort}); + Datatype dtTuple = tupSort.getDatatype(); + EXPECT_TRUE(dtTuple.isTuple()); + EXPECT_FALSE(dtTuple.isRecord()); + EXPECT_TRUE(dtTuple.isFinite()); + EXPECT_TRUE(dtTuple.isWellFounded()); + + // create record + std::vector> fields = { + std::make_pair("b", boolSort), std::make_pair("i", intSort)}; + Sort recSort = d_solver.mkRecordSort(fields); + EXPECT_TRUE(recSort.isDatatype()); + Datatype dtRecord = recSort.getDatatype(); + EXPECT_FALSE(dtRecord.isTuple()); + EXPECT_TRUE(dtRecord.isRecord()); + EXPECT_FALSE(dtRecord.isFinite()); + EXPECT_TRUE(dtRecord.isWellFounded()); +} + +TEST_F(TestApi, datatypeNames) +{ + Sort intSort = d_solver.getIntegerSort(); + + // create datatype sort to test + DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); + ASSERT_NO_THROW(dtypeSpec.getName()); + EXPECT_EQ(dtypeSpec.getName(), std::string("list")); + DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); + cons.addSelector("head", intSort); + cons.addSelectorSelf("tail"); + dtypeSpec.addConstructor(cons); + DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); + dtypeSpec.addConstructor(nil); + Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); + Datatype dt = dtypeSort.getDatatype(); + EXPECT_EQ(dt.getName(), std::string("list")); + ASSERT_NO_THROW(dt.getConstructor("nil")); + ASSERT_NO_THROW(dt["cons"]); + ASSERT_THROW(dt.getConstructor("head"), CVC4ApiException); + ASSERT_THROW(dt.getConstructor(""), CVC4ApiException); + + DatatypeConstructor dcons = dt[0]; + EXPECT_EQ(dcons.getName(), std::string("cons")); + ASSERT_NO_THROW(dcons.getSelector("head")); + ASSERT_NO_THROW(dcons["tail"]); + ASSERT_THROW(dcons.getSelector("cons"), CVC4ApiException); + + // get selector + DatatypeSelector dselTail = dcons[1]; + EXPECT_EQ(dselTail.getName(), std::string("tail")); + EXPECT_EQ(dselTail.getRangeSort(), dtypeSort); + + // possible to construct null datatype declarations if not using solver + ASSERT_THROW(DatatypeDecl().getName(), CVC4ApiException); +} + +TEST_F(TestApi, parametricDatatype) +{ + std::vector v; + Sort t1 = d_solver.mkParamSort("T1"); + Sort t2 = d_solver.mkParamSort("T2"); + v.push_back(t1); + v.push_back(t2); + DatatypeDecl pairSpec = d_solver.mkDatatypeDecl("pair", v); + + DatatypeConstructorDecl mkpair = + d_solver.mkDatatypeConstructorDecl("mk-pair"); + mkpair.addSelector("first", t1); + mkpair.addSelector("second", t2); + pairSpec.addConstructor(mkpair); + + Sort pairType = d_solver.mkDatatypeSort(pairSpec); + + EXPECT_TRUE(pairType.getDatatype().isParametric()); + + v.clear(); + v.push_back(d_solver.getIntegerSort()); + v.push_back(d_solver.getIntegerSort()); + Sort pairIntInt = pairType.instantiate(v); + v.clear(); + v.push_back(d_solver.getRealSort()); + v.push_back(d_solver.getRealSort()); + Sort pairRealReal = pairType.instantiate(v); + v.clear(); + v.push_back(d_solver.getRealSort()); + v.push_back(d_solver.getIntegerSort()); + Sort pairRealInt = pairType.instantiate(v); + v.clear(); + v.push_back(d_solver.getIntegerSort()); + v.push_back(d_solver.getRealSort()); + Sort pairIntReal = pairType.instantiate(v); + + EXPECT_NE(pairIntInt, pairRealReal); + EXPECT_NE(pairIntReal, pairRealReal); + EXPECT_NE(pairRealInt, pairRealReal); + EXPECT_NE(pairIntInt, pairIntReal); + EXPECT_NE(pairIntInt, pairRealInt); + EXPECT_NE(pairIntReal, pairRealInt); + + EXPECT_TRUE(pairRealReal.isComparableTo(pairRealReal)); + EXPECT_FALSE(pairIntReal.isComparableTo(pairRealReal)); + EXPECT_FALSE(pairRealInt.isComparableTo(pairRealReal)); + EXPECT_FALSE(pairIntInt.isComparableTo(pairRealReal)); + EXPECT_FALSE(pairRealReal.isComparableTo(pairRealInt)); + EXPECT_FALSE(pairIntReal.isComparableTo(pairRealInt)); + EXPECT_TRUE(pairRealInt.isComparableTo(pairRealInt)); + EXPECT_FALSE(pairIntInt.isComparableTo(pairRealInt)); + EXPECT_FALSE(pairRealReal.isComparableTo(pairIntReal)); + EXPECT_TRUE(pairIntReal.isComparableTo(pairIntReal)); + EXPECT_FALSE(pairRealInt.isComparableTo(pairIntReal)); + EXPECT_FALSE(pairIntInt.isComparableTo(pairIntReal)); + EXPECT_FALSE(pairRealReal.isComparableTo(pairIntInt)); + EXPECT_FALSE(pairIntReal.isComparableTo(pairIntInt)); + EXPECT_FALSE(pairRealInt.isComparableTo(pairIntInt)); + EXPECT_TRUE(pairIntInt.isComparableTo(pairIntInt)); + + EXPECT_TRUE(pairRealReal.isSubsortOf(pairRealReal)); + EXPECT_FALSE(pairIntReal.isSubsortOf(pairRealReal)); + EXPECT_FALSE(pairRealInt.isSubsortOf(pairRealReal)); + EXPECT_FALSE(pairIntInt.isSubsortOf(pairRealReal)); + EXPECT_FALSE(pairRealReal.isSubsortOf(pairRealInt)); + EXPECT_FALSE(pairIntReal.isSubsortOf(pairRealInt)); + EXPECT_TRUE(pairRealInt.isSubsortOf(pairRealInt)); + EXPECT_FALSE(pairIntInt.isSubsortOf(pairRealInt)); + EXPECT_FALSE(pairRealReal.isSubsortOf(pairIntReal)); + EXPECT_TRUE(pairIntReal.isSubsortOf(pairIntReal)); + EXPECT_FALSE(pairRealInt.isSubsortOf(pairIntReal)); + EXPECT_FALSE(pairIntInt.isSubsortOf(pairIntReal)); + EXPECT_FALSE(pairRealReal.isSubsortOf(pairIntInt)); + EXPECT_FALSE(pairIntReal.isSubsortOf(pairIntInt)); + EXPECT_FALSE(pairRealInt.isSubsortOf(pairIntInt)); + EXPECT_TRUE(pairIntInt.isSubsortOf(pairIntInt)); +} + +TEST_F(TestApi, datatypeSimplyRec) +{ + /* Create mutual datatypes corresponding to this definition block: + * + * DATATYPE + * wlist = leaf(data: list), + * list = cons(car: wlist, cdr: list) | nil, + * ns = elem(ndata: set(wlist)) | elemArray(ndata2: array(list, list)) + * END; + */ + // Make unresolved types as placeholders + std::set unresTypes; + Sort unresWList = d_solver.mkUninterpretedSort("wlist"); + Sort unresList = d_solver.mkUninterpretedSort("list"); + Sort unresNs = d_solver.mkUninterpretedSort("ns"); + unresTypes.insert(unresWList); + unresTypes.insert(unresList); + unresTypes.insert(unresNs); + + DatatypeDecl wlist = d_solver.mkDatatypeDecl("wlist"); + DatatypeConstructorDecl leaf = d_solver.mkDatatypeConstructorDecl("leaf"); + leaf.addSelector("data", unresList); + wlist.addConstructor(leaf); + + DatatypeDecl list = d_solver.mkDatatypeDecl("list"); + DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); + cons.addSelector("car", unresWList); + cons.addSelector("cdr", unresList); + list.addConstructor(cons); + DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); + list.addConstructor(nil); + + DatatypeDecl ns = d_solver.mkDatatypeDecl("ns"); + DatatypeConstructorDecl elem = d_solver.mkDatatypeConstructorDecl("elem"); + elem.addSelector("ndata", d_solver.mkSetSort(unresWList)); + ns.addConstructor(elem); + DatatypeConstructorDecl elemArray = + d_solver.mkDatatypeConstructorDecl("elemArray"); + elemArray.addSelector("ndata", d_solver.mkArraySort(unresList, unresList)); + ns.addConstructor(elemArray); + + std::vector dtdecls; + dtdecls.push_back(wlist); + dtdecls.push_back(list); + dtdecls.push_back(ns); + // this is well-founded and has no nested recursion + std::vector dtsorts; + ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes)); + ASSERT_EQ(dtsorts.size(), 3); + EXPECT_TRUE(dtsorts[0].getDatatype().isWellFounded()); + EXPECT_TRUE(dtsorts[1].getDatatype().isWellFounded()); + EXPECT_TRUE(dtsorts[2].getDatatype().isWellFounded()); + EXPECT_FALSE(dtsorts[0].getDatatype().hasNestedRecursion()); + EXPECT_FALSE(dtsorts[1].getDatatype().hasNestedRecursion()); + EXPECT_FALSE(dtsorts[2].getDatatype().hasNestedRecursion()); + + /* Create mutual datatypes corresponding to this definition block: + * DATATYPE + * ns2 = elem2(ndata: array(int,ns2)) | nil2 + * END; + */ + unresTypes.clear(); + Sort unresNs2 = d_solver.mkUninterpretedSort("ns2"); + unresTypes.insert(unresNs2); + + DatatypeDecl ns2 = d_solver.mkDatatypeDecl("ns2"); + DatatypeConstructorDecl elem2 = d_solver.mkDatatypeConstructorDecl("elem2"); + elem2.addSelector("ndata", + d_solver.mkArraySort(d_solver.getIntegerSort(), unresNs2)); + ns2.addConstructor(elem2); + DatatypeConstructorDecl nil2 = d_solver.mkDatatypeConstructorDecl("nil2"); + ns2.addConstructor(nil2); + + dtdecls.clear(); + dtdecls.push_back(ns2); + + dtsorts.clear(); + // this is not well-founded due to non-simple recursion + ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes)); + ASSERT_EQ(dtsorts.size(), 1); + ASSERT_TRUE(dtsorts[0].getDatatype()[0][0].getRangeSort().isArray()); + EXPECT_EQ(dtsorts[0].getDatatype()[0][0].getRangeSort().getArrayElementSort(), + dtsorts[0]); + EXPECT_TRUE(dtsorts[0].getDatatype().isWellFounded()); + EXPECT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion()); + + /* Create mutual datatypes corresponding to this definition block: + * DATATYPE + * list3 = cons3(car: ns3, cdr: list3) | nil3, + * ns3 = elem3(ndata: set(list3)) + * END; + */ + unresTypes.clear(); + Sort unresNs3 = d_solver.mkUninterpretedSort("ns3"); + unresTypes.insert(unresNs3); + Sort unresList3 = d_solver.mkUninterpretedSort("list3"); + unresTypes.insert(unresList3); + + DatatypeDecl list3 = d_solver.mkDatatypeDecl("list3"); + DatatypeConstructorDecl cons3 = d_solver.mkDatatypeConstructorDecl("cons3"); + cons3.addSelector("car", unresNs3); + cons3.addSelector("cdr", unresList3); + list3.addConstructor(cons3); + DatatypeConstructorDecl nil3 = d_solver.mkDatatypeConstructorDecl("nil3"); + list3.addConstructor(nil3); + + DatatypeDecl ns3 = d_solver.mkDatatypeDecl("ns3"); + DatatypeConstructorDecl elem3 = d_solver.mkDatatypeConstructorDecl("elem3"); + elem3.addSelector("ndata", d_solver.mkSetSort(unresList3)); + ns3.addConstructor(elem3); + + dtdecls.clear(); + dtdecls.push_back(list3); + dtdecls.push_back(ns3); + + dtsorts.clear(); + // both are well-founded and have nested recursion + ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes)); + ASSERT_EQ(dtsorts.size(), 2); + EXPECT_TRUE(dtsorts[0].getDatatype().isWellFounded()); + EXPECT_TRUE(dtsorts[1].getDatatype().isWellFounded()); + EXPECT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion()); + EXPECT_TRUE(dtsorts[1].getDatatype().hasNestedRecursion()); + + /* Create mutual datatypes corresponding to this definition block: + * DATATYPE + * list4 = cons(car: set(ns4), cdr: list4) | nil, + * ns4 = elem(ndata: list4) + * END; + */ + unresTypes.clear(); + Sort unresNs4 = d_solver.mkUninterpretedSort("ns4"); + unresTypes.insert(unresNs4); + Sort unresList4 = d_solver.mkUninterpretedSort("list4"); + unresTypes.insert(unresList4); + + DatatypeDecl list4 = d_solver.mkDatatypeDecl("list4"); + DatatypeConstructorDecl cons4 = d_solver.mkDatatypeConstructorDecl("cons4"); + cons4.addSelector("car", d_solver.mkSetSort(unresNs4)); + cons4.addSelector("cdr", unresList4); + list4.addConstructor(cons4); + DatatypeConstructorDecl nil4 = d_solver.mkDatatypeConstructorDecl("nil4"); + list4.addConstructor(nil4); + + DatatypeDecl ns4 = d_solver.mkDatatypeDecl("ns4"); + DatatypeConstructorDecl elem4 = d_solver.mkDatatypeConstructorDecl("elem3"); + elem4.addSelector("ndata", unresList4); + ns4.addConstructor(elem4); + + dtdecls.clear(); + dtdecls.push_back(list4); + dtdecls.push_back(ns4); + + dtsorts.clear(); + // both are well-founded and have nested recursion + ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes)); + ASSERT_EQ(dtsorts.size(), 2); + EXPECT_TRUE(dtsorts[0].getDatatype().isWellFounded()); + EXPECT_TRUE(dtsorts[1].getDatatype().isWellFounded()); + EXPECT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion()); + EXPECT_TRUE(dtsorts[1].getDatatype().hasNestedRecursion()); + + /* Create mutual datatypes corresponding to this definition block: + * DATATYPE + * list5[X] = cons(car: X, cdr: list5[list5[X]]) | nil + * END; + */ + unresTypes.clear(); + Sort unresList5 = d_solver.mkSortConstructorSort("list5", 1); + unresTypes.insert(unresList5); + + std::vector v; + Sort x = d_solver.mkParamSort("X"); + v.push_back(x); + DatatypeDecl list5 = d_solver.mkDatatypeDecl("list5", v); + + std::vector args; + args.push_back(x); + Sort urListX = unresList5.instantiate(args); + args[0] = urListX; + Sort urListListX = unresList5.instantiate(args); + + DatatypeConstructorDecl cons5 = d_solver.mkDatatypeConstructorDecl("cons5"); + cons5.addSelector("car", x); + cons5.addSelector("cdr", urListListX); + list5.addConstructor(cons5); + DatatypeConstructorDecl nil5 = d_solver.mkDatatypeConstructorDecl("nil5"); + list5.addConstructor(nil5); + + dtdecls.clear(); + dtdecls.push_back(list5); + + // well-founded and has nested recursion + ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes)); + ASSERT_EQ(dtsorts.size(), 1); + EXPECT_TRUE(dtsorts[0].getDatatype().isWellFounded()); + EXPECT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion()); +} + +TEST_F(TestApi, datatypeSpecializedCons) +{ + /* Create mutual datatypes corresponding to this definition block: + * DATATYPE + * plist[X] = pcons(car: X, cdr: plist[X]) | pnil + * END; + */ + // Make unresolved types as placeholders + std::set unresTypes; + Sort unresList = d_solver.mkSortConstructorSort("plist", 1); + unresTypes.insert(unresList); + + std::vector v; + Sort x = d_solver.mkParamSort("X"); + v.push_back(x); + DatatypeDecl plist = d_solver.mkDatatypeDecl("plist", v); + + std::vector args; + args.push_back(x); + Sort urListX = unresList.instantiate(args); + + DatatypeConstructorDecl pcons = d_solver.mkDatatypeConstructorDecl("pcons"); + pcons.addSelector("car", x); + pcons.addSelector("cdr", urListX); + plist.addConstructor(pcons); + DatatypeConstructorDecl nil5 = d_solver.mkDatatypeConstructorDecl("pnil"); + plist.addConstructor(nil5); + + std::vector dtdecls; + dtdecls.push_back(plist); + + std::vector dtsorts; + // make the datatype sorts + ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes)); + ASSERT_EQ(dtsorts.size(), 1); + Datatype d = dtsorts[0].getDatatype(); + DatatypeConstructor nilc = d[0]; + + Sort isort = d_solver.getIntegerSort(); + std::vector iargs; + iargs.push_back(isort); + Sort listInt = dtsorts[0].instantiate(iargs); + + Term testConsTerm; + // get the specialized constructor term for list[Int] + ASSERT_NO_THROW(testConsTerm = nilc.getSpecializedConstructorTerm(listInt)); + EXPECT_NE(testConsTerm, nilc.getConstructorTerm()); + // error to get the specialized constructor term for Int + EXPECT_THROW(nilc.getSpecializedConstructorTerm(isort), CVC4ApiException); +} diff --git a/test/unit/api/datatype_api_black.h b/test/unit/api/datatype_api_black.h deleted file mode 100644 index 4564b261a..000000000 --- a/test/unit/api/datatype_api_black.h +++ /dev/null @@ -1,576 +0,0 @@ -/********************* */ -/*! \file datatype_api_black.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Aina Niemetz, Andres Noetzli - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 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 Black box testing of the datatype classes of the C++ API. - ** - ** Black box testing of the datatype classes of the C++ API. - **/ - -#include - -#include "api/cvc4cpp.h" - -using namespace CVC4::api; - -class DatatypeBlack : public CxxTest::TestSuite -{ - public: - void setUp() override; - void tearDown() override; - - void testMkDatatypeSort(); - void testMkDatatypeSorts(); - - void testDatatypeStructs(); - void testDatatypeNames(); - - void testParametricDatatype(); - - void testDatatypeSimplyRec(); - - void testDatatypeSpecializedCons(); - - private: - Solver d_solver; -}; - -void DatatypeBlack::setUp() {} - -void DatatypeBlack::tearDown() {} - -void DatatypeBlack::testMkDatatypeSort() -{ - DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); - DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); - cons.addSelector("head", d_solver.getIntegerSort()); - dtypeSpec.addConstructor(cons); - DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); - dtypeSpec.addConstructor(nil); - Sort listSort = d_solver.mkDatatypeSort(dtypeSpec); - Datatype d = listSort.getDatatype(); - DatatypeConstructor consConstr = d[0]; - DatatypeConstructor nilConstr = d[1]; - TS_ASSERT_THROWS(d[2], CVC4ApiException&); - TS_ASSERT_THROWS_NOTHING(consConstr.getConstructorTerm()); - TS_ASSERT_THROWS_NOTHING(nilConstr.getConstructorTerm()); -} - -void DatatypeBlack::testMkDatatypeSorts() -{ - /* Create two mutual datatypes corresponding to this definition - * block: - * - * DATATYPE - * tree = node(left: tree, right: tree) | leaf(data: list), - * list = cons(car: tree, cdr: list) | nil - * END; - */ - // Make unresolved types as placeholders - std::set unresTypes; - Sort unresTree = d_solver.mkUninterpretedSort("tree"); - Sort unresList = d_solver.mkUninterpretedSort("list"); - unresTypes.insert(unresTree); - unresTypes.insert(unresList); - - DatatypeDecl tree = d_solver.mkDatatypeDecl("tree"); - DatatypeConstructorDecl node = d_solver.mkDatatypeConstructorDecl("node"); - node.addSelector("left", unresTree); - node.addSelector("right", unresTree); - tree.addConstructor(node); - - DatatypeConstructorDecl leaf = d_solver.mkDatatypeConstructorDecl("leaf"); - leaf.addSelector("data", unresList); - tree.addConstructor(leaf); - - DatatypeDecl list = d_solver.mkDatatypeDecl("list"); - DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); - cons.addSelector("car", unresTree); - cons.addSelector("cdr", unresTree); - list.addConstructor(cons); - - DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); - list.addConstructor(nil); - - std::vector dtdecls; - dtdecls.push_back(tree); - dtdecls.push_back(list); - std::vector dtsorts; - TS_ASSERT_THROWS_NOTHING(dtsorts = - d_solver.mkDatatypeSorts(dtdecls, unresTypes)); - TS_ASSERT(dtsorts.size() == dtdecls.size()); - for (unsigned i = 0, ndecl = dtdecls.size(); i < ndecl; i++) - { - TS_ASSERT(dtsorts[i].isDatatype()); - TS_ASSERT(!dtsorts[i].getDatatype().isFinite()); - TS_ASSERT(dtsorts[i].getDatatype().getName() == dtdecls[i].getName()); - } - // verify the resolution was correct - Datatype dtTree = dtsorts[0].getDatatype(); - DatatypeConstructor dtcTreeNode = dtTree[0]; - TS_ASSERT(dtcTreeNode.getName() == "node"); - DatatypeSelector dtsTreeNodeLeft = dtcTreeNode[0]; - TS_ASSERT(dtsTreeNodeLeft.getName() == "left"); - // argument type should have resolved to be recursive - TS_ASSERT(dtsTreeNodeLeft.getRangeSort().isDatatype()); - TS_ASSERT(dtsTreeNodeLeft.getRangeSort() == dtsorts[0]); - - // fails due to empty datatype - std::vector dtdeclsBad; - DatatypeDecl emptyD = d_solver.mkDatatypeDecl("emptyD"); - dtdeclsBad.push_back(emptyD); - TS_ASSERT_THROWS(d_solver.mkDatatypeSorts(dtdeclsBad), CVC4ApiException&); -} - -void DatatypeBlack::testDatatypeStructs() -{ - Sort intSort = d_solver.getIntegerSort(); - Sort boolSort = d_solver.getBooleanSort(); - - // create datatype sort to test - DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); - DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); - cons.addSelector("head", intSort); - cons.addSelectorSelf("tail"); - Sort nullSort; - TS_ASSERT_THROWS(cons.addSelector("null", nullSort), CVC4ApiException&); - dtypeSpec.addConstructor(cons); - DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); - dtypeSpec.addConstructor(nil); - Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); - Datatype dt = dtypeSort.getDatatype(); - TS_ASSERT(!dt.isCodatatype()); - TS_ASSERT(!dt.isTuple()); - TS_ASSERT(!dt.isRecord()); - TS_ASSERT(!dt.isFinite()); - TS_ASSERT(dt.isWellFounded()); - // get constructor - DatatypeConstructor dcons = dt[0]; - Term consTerm = dcons.getConstructorTerm(); - TS_ASSERT(dcons.getNumSelectors() == 2); - - // create datatype sort to test - DatatypeDecl dtypeSpecEnum = d_solver.mkDatatypeDecl("enum"); - DatatypeConstructorDecl ca = d_solver.mkDatatypeConstructorDecl("A"); - dtypeSpecEnum.addConstructor(ca); - DatatypeConstructorDecl cb = d_solver.mkDatatypeConstructorDecl("B"); - dtypeSpecEnum.addConstructor(cb); - DatatypeConstructorDecl cc = d_solver.mkDatatypeConstructorDecl("C"); - dtypeSpecEnum.addConstructor(cc); - Sort dtypeSortEnum = d_solver.mkDatatypeSort(dtypeSpecEnum); - Datatype dtEnum = dtypeSortEnum.getDatatype(); - TS_ASSERT(!dtEnum.isTuple()); - TS_ASSERT(dtEnum.isFinite()); - - // create codatatype - DatatypeDecl dtypeSpecStream = d_solver.mkDatatypeDecl("stream", true); - DatatypeConstructorDecl consStream = - d_solver.mkDatatypeConstructorDecl("cons"); - consStream.addSelector("head", intSort); - consStream.addSelectorSelf("tail"); - dtypeSpecStream.addConstructor(consStream); - Sort dtypeSortStream = d_solver.mkDatatypeSort(dtypeSpecStream); - Datatype dtStream = dtypeSortStream.getDatatype(); - TS_ASSERT(dtStream.isCodatatype()); - TS_ASSERT(!dtStream.isFinite()); - // codatatypes may be well-founded - TS_ASSERT(dtStream.isWellFounded()); - - // create tuple - Sort tupSort = d_solver.mkTupleSort({boolSort}); - Datatype dtTuple = tupSort.getDatatype(); - TS_ASSERT(dtTuple.isTuple()); - TS_ASSERT(!dtTuple.isRecord()); - TS_ASSERT(dtTuple.isFinite()); - TS_ASSERT(dtTuple.isWellFounded()); - - // create record - std::vector> fields = { - std::make_pair("b", boolSort), std::make_pair("i", intSort)}; - Sort recSort = d_solver.mkRecordSort(fields); - TS_ASSERT(recSort.isDatatype()); - Datatype dtRecord = recSort.getDatatype(); - TS_ASSERT(!dtRecord.isTuple()); - TS_ASSERT(dtRecord.isRecord()); - TS_ASSERT(!dtRecord.isFinite()); - TS_ASSERT(dtRecord.isWellFounded()); -} - -void DatatypeBlack::testDatatypeNames() -{ - Sort intSort = d_solver.getIntegerSort(); - - // create datatype sort to test - DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); - TS_ASSERT_THROWS_NOTHING(dtypeSpec.getName()); - TS_ASSERT(dtypeSpec.getName() == std::string("list")); - DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); - cons.addSelector("head", intSort); - cons.addSelectorSelf("tail"); - dtypeSpec.addConstructor(cons); - DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); - dtypeSpec.addConstructor(nil); - Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); - Datatype dt = dtypeSort.getDatatype(); - TS_ASSERT(dt.getName() == std::string("list")); - TS_ASSERT_THROWS_NOTHING(dt.getConstructor("nil")); - TS_ASSERT_THROWS_NOTHING(dt["cons"]); - TS_ASSERT_THROWS(dt.getConstructor("head"), CVC4ApiException&); - TS_ASSERT_THROWS(dt.getConstructor(""), CVC4ApiException&); - - DatatypeConstructor dcons = dt[0]; - TS_ASSERT(dcons.getName() == std::string("cons")); - TS_ASSERT_THROWS_NOTHING(dcons.getSelector("head")); - TS_ASSERT_THROWS_NOTHING(dcons["tail"]); - TS_ASSERT_THROWS(dcons.getSelector("cons"), CVC4ApiException&); - - // get selector - DatatypeSelector dselTail = dcons[1]; - TS_ASSERT(dselTail.getName() == std::string("tail")); - TS_ASSERT(dselTail.getRangeSort() == dtypeSort); - - // possible to construct null datatype declarations if not using solver - TS_ASSERT_THROWS(DatatypeDecl().getName(), CVC4ApiException&); -} - -void DatatypeBlack::testParametricDatatype() -{ - std::vector v; - Sort t1 = d_solver.mkParamSort("T1"); - Sort t2 = d_solver.mkParamSort("T2"); - v.push_back(t1); - v.push_back(t2); - DatatypeDecl pairSpec = d_solver.mkDatatypeDecl("pair", v); - - DatatypeConstructorDecl mkpair = - d_solver.mkDatatypeConstructorDecl("mk-pair"); - mkpair.addSelector("first", t1); - mkpair.addSelector("second", t2); - pairSpec.addConstructor(mkpair); - - Sort pairType = d_solver.mkDatatypeSort(pairSpec); - - TS_ASSERT(pairType.getDatatype().isParametric()); - - v.clear(); - v.push_back(d_solver.getIntegerSort()); - v.push_back(d_solver.getIntegerSort()); - Sort pairIntInt = pairType.instantiate(v); - v.clear(); - v.push_back(d_solver.getRealSort()); - v.push_back(d_solver.getRealSort()); - Sort pairRealReal = pairType.instantiate(v); - v.clear(); - v.push_back(d_solver.getRealSort()); - v.push_back(d_solver.getIntegerSort()); - Sort pairRealInt = pairType.instantiate(v); - v.clear(); - v.push_back(d_solver.getIntegerSort()); - v.push_back(d_solver.getRealSort()); - Sort pairIntReal = pairType.instantiate(v); - - TS_ASSERT_DIFFERS(pairIntInt, pairRealReal); - TS_ASSERT_DIFFERS(pairIntReal, pairRealReal); - TS_ASSERT_DIFFERS(pairRealInt, pairRealReal); - TS_ASSERT_DIFFERS(pairIntInt, pairIntReal); - TS_ASSERT_DIFFERS(pairIntInt, pairRealInt); - TS_ASSERT_DIFFERS(pairIntReal, pairRealInt); - - TS_ASSERT(pairRealReal.isComparableTo(pairRealReal)); - TS_ASSERT(!pairIntReal.isComparableTo(pairRealReal)); - TS_ASSERT(!pairRealInt.isComparableTo(pairRealReal)); - TS_ASSERT(!pairIntInt.isComparableTo(pairRealReal)); - TS_ASSERT(!pairRealReal.isComparableTo(pairRealInt)); - TS_ASSERT(!pairIntReal.isComparableTo(pairRealInt)); - TS_ASSERT(pairRealInt.isComparableTo(pairRealInt)); - TS_ASSERT(!pairIntInt.isComparableTo(pairRealInt)); - TS_ASSERT(!pairRealReal.isComparableTo(pairIntReal)); - TS_ASSERT(pairIntReal.isComparableTo(pairIntReal)); - TS_ASSERT(!pairRealInt.isComparableTo(pairIntReal)); - TS_ASSERT(!pairIntInt.isComparableTo(pairIntReal)); - TS_ASSERT(!pairRealReal.isComparableTo(pairIntInt)); - TS_ASSERT(!pairIntReal.isComparableTo(pairIntInt)); - TS_ASSERT(!pairRealInt.isComparableTo(pairIntInt)); - TS_ASSERT(pairIntInt.isComparableTo(pairIntInt)); - - TS_ASSERT(pairRealReal.isSubsortOf(pairRealReal)); - TS_ASSERT(!pairIntReal.isSubsortOf(pairRealReal)); - TS_ASSERT(!pairRealInt.isSubsortOf(pairRealReal)); - TS_ASSERT(!pairIntInt.isSubsortOf(pairRealReal)); - TS_ASSERT(!pairRealReal.isSubsortOf(pairRealInt)); - TS_ASSERT(!pairIntReal.isSubsortOf(pairRealInt)); - TS_ASSERT(pairRealInt.isSubsortOf(pairRealInt)); - TS_ASSERT(!pairIntInt.isSubsortOf(pairRealInt)); - TS_ASSERT(!pairRealReal.isSubsortOf(pairIntReal)); - TS_ASSERT(pairIntReal.isSubsortOf(pairIntReal)); - TS_ASSERT(!pairRealInt.isSubsortOf(pairIntReal)); - TS_ASSERT(!pairIntInt.isSubsortOf(pairIntReal)); - TS_ASSERT(!pairRealReal.isSubsortOf(pairIntInt)); - TS_ASSERT(!pairIntReal.isSubsortOf(pairIntInt)); - TS_ASSERT(!pairRealInt.isSubsortOf(pairIntInt)); - TS_ASSERT(pairIntInt.isSubsortOf(pairIntInt)); -} - -void DatatypeBlack::testDatatypeSimplyRec() -{ - /* Create mutual datatypes corresponding to this definition block: - * - * DATATYPE - * wlist = leaf(data: list), - * list = cons(car: wlist, cdr: list) | nil, - * ns = elem(ndata: set(wlist)) | elemArray(ndata2: array(list, list)) - * END; - */ - // Make unresolved types as placeholders - std::set unresTypes; - Sort unresWList = d_solver.mkUninterpretedSort("wlist"); - Sort unresList = d_solver.mkUninterpretedSort("list"); - Sort unresNs = d_solver.mkUninterpretedSort("ns"); - unresTypes.insert(unresWList); - unresTypes.insert(unresList); - unresTypes.insert(unresNs); - - DatatypeDecl wlist = d_solver.mkDatatypeDecl("wlist"); - DatatypeConstructorDecl leaf = d_solver.mkDatatypeConstructorDecl("leaf"); - leaf.addSelector("data", unresList); - wlist.addConstructor(leaf); - - DatatypeDecl list = d_solver.mkDatatypeDecl("list"); - DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); - cons.addSelector("car", unresWList); - cons.addSelector("cdr", unresList); - list.addConstructor(cons); - DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); - list.addConstructor(nil); - - DatatypeDecl ns = d_solver.mkDatatypeDecl("ns"); - DatatypeConstructorDecl elem = d_solver.mkDatatypeConstructorDecl("elem"); - elem.addSelector("ndata", d_solver.mkSetSort(unresWList)); - ns.addConstructor(elem); - DatatypeConstructorDecl elemArray = - d_solver.mkDatatypeConstructorDecl("elemArray"); - elemArray.addSelector("ndata", d_solver.mkArraySort(unresList, unresList)); - ns.addConstructor(elemArray); - - std::vector dtdecls; - dtdecls.push_back(wlist); - dtdecls.push_back(list); - dtdecls.push_back(ns); - // this is well-founded and has no nested recursion - std::vector dtsorts; - TS_ASSERT_THROWS_NOTHING(dtsorts = - d_solver.mkDatatypeSorts(dtdecls, unresTypes)); - TS_ASSERT(dtsorts.size() == 3); - TS_ASSERT(dtsorts[0].getDatatype().isWellFounded()); - TS_ASSERT(dtsorts[1].getDatatype().isWellFounded()); - TS_ASSERT(dtsorts[2].getDatatype().isWellFounded()); - TS_ASSERT(!dtsorts[0].getDatatype().hasNestedRecursion()); - TS_ASSERT(!dtsorts[1].getDatatype().hasNestedRecursion()); - TS_ASSERT(!dtsorts[2].getDatatype().hasNestedRecursion()); - - /* Create mutual datatypes corresponding to this definition block: - * DATATYPE - * ns2 = elem2(ndata: array(int,ns2)) | nil2 - * END; - */ - unresTypes.clear(); - Sort unresNs2 = d_solver.mkUninterpretedSort("ns2"); - unresTypes.insert(unresNs2); - - DatatypeDecl ns2 = d_solver.mkDatatypeDecl("ns2"); - DatatypeConstructorDecl elem2 = d_solver.mkDatatypeConstructorDecl("elem2"); - elem2.addSelector("ndata", - d_solver.mkArraySort(d_solver.getIntegerSort(), unresNs2)); - ns2.addConstructor(elem2); - DatatypeConstructorDecl nil2 = d_solver.mkDatatypeConstructorDecl("nil2"); - ns2.addConstructor(nil2); - - dtdecls.clear(); - dtdecls.push_back(ns2); - - dtsorts.clear(); - // this is not well-founded due to non-simple recursion - TS_ASSERT_THROWS_NOTHING(dtsorts = - d_solver.mkDatatypeSorts(dtdecls, unresTypes)); - TS_ASSERT(dtsorts.size() == 1); - TS_ASSERT(dtsorts[0].getDatatype()[0][0].getRangeSort().isArray()); - TS_ASSERT(dtsorts[0].getDatatype()[0][0].getRangeSort().getArrayElementSort() - == dtsorts[0]); - TS_ASSERT(dtsorts[0].getDatatype().isWellFounded()); - TS_ASSERT(dtsorts[0].getDatatype().hasNestedRecursion()); - - /* Create mutual datatypes corresponding to this definition block: - * DATATYPE - * list3 = cons3(car: ns3, cdr: list3) | nil3, - * ns3 = elem3(ndata: set(list3)) - * END; - */ - unresTypes.clear(); - Sort unresNs3 = d_solver.mkUninterpretedSort("ns3"); - unresTypes.insert(unresNs3); - Sort unresList3 = d_solver.mkUninterpretedSort("list3"); - unresTypes.insert(unresList3); - - DatatypeDecl list3 = d_solver.mkDatatypeDecl("list3"); - DatatypeConstructorDecl cons3 = d_solver.mkDatatypeConstructorDecl("cons3"); - cons3.addSelector("car", unresNs3); - cons3.addSelector("cdr", unresList3); - list3.addConstructor(cons3); - DatatypeConstructorDecl nil3 = d_solver.mkDatatypeConstructorDecl("nil3"); - list3.addConstructor(nil3); - - DatatypeDecl ns3 = d_solver.mkDatatypeDecl("ns3"); - DatatypeConstructorDecl elem3 = d_solver.mkDatatypeConstructorDecl("elem3"); - elem3.addSelector("ndata", d_solver.mkSetSort(unresList3)); - ns3.addConstructor(elem3); - - dtdecls.clear(); - dtdecls.push_back(list3); - dtdecls.push_back(ns3); - - dtsorts.clear(); - // both are well-founded and have nested recursion - TS_ASSERT_THROWS_NOTHING(dtsorts = - d_solver.mkDatatypeSorts(dtdecls, unresTypes)); - TS_ASSERT(dtsorts.size() == 2); - TS_ASSERT(dtsorts[0].getDatatype().isWellFounded()); - TS_ASSERT(dtsorts[1].getDatatype().isWellFounded()); - TS_ASSERT(dtsorts[0].getDatatype().hasNestedRecursion()); - TS_ASSERT(dtsorts[1].getDatatype().hasNestedRecursion()); - - /* Create mutual datatypes corresponding to this definition block: - * DATATYPE - * list4 = cons(car: set(ns4), cdr: list4) | nil, - * ns4 = elem(ndata: list4) - * END; - */ - unresTypes.clear(); - Sort unresNs4 = d_solver.mkUninterpretedSort("ns4"); - unresTypes.insert(unresNs4); - Sort unresList4 = d_solver.mkUninterpretedSort("list4"); - unresTypes.insert(unresList4); - - DatatypeDecl list4 = d_solver.mkDatatypeDecl("list4"); - DatatypeConstructorDecl cons4 = d_solver.mkDatatypeConstructorDecl("cons4"); - cons4.addSelector("car", d_solver.mkSetSort(unresNs4)); - cons4.addSelector("cdr", unresList4); - list4.addConstructor(cons4); - DatatypeConstructorDecl nil4 = d_solver.mkDatatypeConstructorDecl("nil4"); - list4.addConstructor(nil4); - - DatatypeDecl ns4 = d_solver.mkDatatypeDecl("ns4"); - DatatypeConstructorDecl elem4 = d_solver.mkDatatypeConstructorDecl("elem3"); - elem4.addSelector("ndata", unresList4); - ns4.addConstructor(elem4); - - dtdecls.clear(); - dtdecls.push_back(list4); - dtdecls.push_back(ns4); - - dtsorts.clear(); - // both are well-founded and have nested recursion - TS_ASSERT_THROWS_NOTHING(dtsorts = - d_solver.mkDatatypeSorts(dtdecls, unresTypes)); - TS_ASSERT(dtsorts.size() == 2); - TS_ASSERT(dtsorts[0].getDatatype().isWellFounded()); - TS_ASSERT(dtsorts[1].getDatatype().isWellFounded()); - TS_ASSERT(dtsorts[0].getDatatype().hasNestedRecursion()); - TS_ASSERT(dtsorts[1].getDatatype().hasNestedRecursion()); - - /* Create mutual datatypes corresponding to this definition block: - * DATATYPE - * list5[X] = cons(car: X, cdr: list5[list5[X]]) | nil - * END; - */ - unresTypes.clear(); - Sort unresList5 = d_solver.mkSortConstructorSort("list5", 1); - unresTypes.insert(unresList5); - - std::vector v; - Sort x = d_solver.mkParamSort("X"); - v.push_back(x); - DatatypeDecl list5 = d_solver.mkDatatypeDecl("list5", v); - - std::vector args; - args.push_back(x); - Sort urListX = unresList5.instantiate(args); - args[0] = urListX; - Sort urListListX = unresList5.instantiate(args); - - DatatypeConstructorDecl cons5 = d_solver.mkDatatypeConstructorDecl("cons5"); - cons5.addSelector("car", x); - cons5.addSelector("cdr", urListListX); - list5.addConstructor(cons5); - DatatypeConstructorDecl nil5 = d_solver.mkDatatypeConstructorDecl("nil5"); - list5.addConstructor(nil5); - - dtdecls.clear(); - dtdecls.push_back(list5); - - // well-founded and has nested recursion - TS_ASSERT_THROWS_NOTHING(dtsorts = - d_solver.mkDatatypeSorts(dtdecls, unresTypes)); - TS_ASSERT(dtsorts.size() == 1); - TS_ASSERT(dtsorts[0].getDatatype().isWellFounded()); - TS_ASSERT(dtsorts[0].getDatatype().hasNestedRecursion()); -} - -void DatatypeBlack::testDatatypeSpecializedCons() -{ - /* Create mutual datatypes corresponding to this definition block: - * DATATYPE - * plist[X] = pcons(car: X, cdr: plist[X]) | pnil - * END; - */ - // Make unresolved types as placeholders - std::set unresTypes; - Sort unresList = d_solver.mkSortConstructorSort("plist", 1); - unresTypes.insert(unresList); - - std::vector v; - Sort x = d_solver.mkParamSort("X"); - v.push_back(x); - DatatypeDecl plist = d_solver.mkDatatypeDecl("plist", v); - - std::vector args; - args.push_back(x); - Sort urListX = unresList.instantiate(args); - - DatatypeConstructorDecl pcons = d_solver.mkDatatypeConstructorDecl("pcons"); - pcons.addSelector("car", x); - pcons.addSelector("cdr", urListX); - plist.addConstructor(pcons); - DatatypeConstructorDecl nil5 = d_solver.mkDatatypeConstructorDecl("pnil"); - plist.addConstructor(nil5); - - std::vector dtdecls; - dtdecls.push_back(plist); - - std::vector dtsorts; - // make the datatype sorts - TS_ASSERT_THROWS_NOTHING(dtsorts = - d_solver.mkDatatypeSorts(dtdecls, unresTypes)); - TS_ASSERT(dtsorts.size() == 1); - Datatype d = dtsorts[0].getDatatype(); - DatatypeConstructor nilc = d[0]; - - Sort isort = d_solver.getIntegerSort(); - std::vector iargs; - iargs.push_back(isort); - Sort listInt = dtsorts[0].instantiate(iargs); - - Term testConsTerm; - // get the specialized constructor term for list[Int] - TS_ASSERT_THROWS_NOTHING(testConsTerm = - nilc.getSpecializedConstructorTerm(listInt)); - TS_ASSERT(testConsTerm != nilc.getConstructorTerm()); - // error to get the specialized constructor term for Int - TS_ASSERT_THROWS(nilc.getSpecializedConstructorTerm(isort), CVC4ApiException&); -} diff --git a/test/unit/base/CMakeLists.txt b/test/unit/base/CMakeLists.txt index 81d27c040..8274a5a46 100644 --- a/test/unit/base/CMakeLists.txt +++ b/test/unit/base/CMakeLists.txt @@ -11,4 +11,4 @@ #-----------------------------------------------------------------------------# # Add unit tests -cvc4_add_unit_test_black(map_util_black base) +cvc4_add_cxx_unit_test_black(map_util_black base) diff --git a/test/unit/context/CMakeLists.txt b/test/unit/context/CMakeLists.txt index 6752f0e78..51465c622 100644 --- a/test/unit/context/CMakeLists.txt +++ b/test/unit/context/CMakeLists.txt @@ -11,10 +11,10 @@ #-----------------------------------------------------------------------------# # Add unit tests -cvc4_add_unit_test_black(cdlist_black context) -cvc4_add_unit_test_black(cdmap_black context) -cvc4_add_unit_test_white(cdmap_white context) -cvc4_add_unit_test_black(cdo_black context) -cvc4_add_unit_test_black(context_black context) -cvc4_add_unit_test_black(context_mm_black context) -cvc4_add_unit_test_white(context_white context) +cvc4_add_cxx_unit_test_black(cdlist_black context) +cvc4_add_cxx_unit_test_black(cdmap_black context) +cvc4_add_cxx_unit_test_white(cdmap_white context) +cvc4_add_cxx_unit_test_black(cdo_black context) +cvc4_add_cxx_unit_test_black(context_black context) +cvc4_add_cxx_unit_test_black(context_mm_black context) +cvc4_add_cxx_unit_test_white(context_white context) diff --git a/test/unit/expr/CMakeLists.txt b/test/unit/expr/CMakeLists.txt index c10648c03..6c0abc4ab 100644 --- a/test/unit/expr/CMakeLists.txt +++ b/test/unit/expr/CMakeLists.txt @@ -11,20 +11,20 @@ #-----------------------------------------------------------------------------# # Add unit tests -cvc4_add_unit_test_black(attribute_black expr) -cvc4_add_unit_test_white(attribute_white expr) -cvc4_add_unit_test_black(expr_manager_public expr) -cvc4_add_unit_test_black(expr_public expr) -cvc4_add_unit_test_black(kind_black expr) -cvc4_add_unit_test_black(kind_map_black expr) -cvc4_add_unit_test_black(node_black expr) -cvc4_add_unit_test_black(node_algorithm_black expr) -cvc4_add_unit_test_black(node_builder_black expr) -cvc4_add_unit_test_black(node_manager_black expr) -cvc4_add_unit_test_white(node_manager_white expr) -cvc4_add_unit_test_black(node_self_iterator_black expr) -cvc4_add_unit_test_black(node_traversal_black expr) -cvc4_add_unit_test_white(node_white expr) -cvc4_add_unit_test_black(symbol_table_black expr) -cvc4_add_unit_test_black(type_cardinality_public expr) -cvc4_add_unit_test_white(type_node_white expr) +cvc4_add_cxx_unit_test_black(attribute_black expr) +cvc4_add_cxx_unit_test_white(attribute_white expr) +cvc4_add_cxx_unit_test_black(expr_manager_public expr) +cvc4_add_cxx_unit_test_black(expr_public expr) +cvc4_add_cxx_unit_test_black(kind_black expr) +cvc4_add_cxx_unit_test_black(kind_map_black expr) +cvc4_add_cxx_unit_test_black(node_black expr) +cvc4_add_cxx_unit_test_black(node_algorithm_black expr) +cvc4_add_cxx_unit_test_black(node_builder_black expr) +cvc4_add_cxx_unit_test_black(node_manager_black expr) +cvc4_add_cxx_unit_test_white(node_manager_white expr) +cvc4_add_cxx_unit_test_black(node_self_iterator_black expr) +cvc4_add_cxx_unit_test_black(node_traversal_black expr) +cvc4_add_cxx_unit_test_white(node_white expr) +cvc4_add_cxx_unit_test_black(symbol_table_black expr) +cvc4_add_cxx_unit_test_black(type_cardinality_public expr) +cvc4_add_cxx_unit_test_white(type_node_white expr) diff --git a/test/unit/main/CMakeLists.txt b/test/unit/main/CMakeLists.txt index 55307db95..59c197f04 100644 --- a/test/unit/main/CMakeLists.txt +++ b/test/unit/main/CMakeLists.txt @@ -11,4 +11,4 @@ #-----------------------------------------------------------------------------# # Add unit tests -cvc4_add_unit_test_black(interactive_shell_black main) +cvc4_add_cxx_unit_test_black(interactive_shell_black main) diff --git a/test/unit/parser/CMakeLists.txt b/test/unit/parser/CMakeLists.txt index 1bdcbd5f5..4202ea0c9 100644 --- a/test/unit/parser/CMakeLists.txt +++ b/test/unit/parser/CMakeLists.txt @@ -11,5 +11,5 @@ #-----------------------------------------------------------------------------# # Add unit tests -cvc4_add_unit_test_black(parser_black parser) -cvc4_add_unit_test_black(parser_builder_black parser) +cvc4_add_cxx_unit_test_black(parser_black parser) +cvc4_add_cxx_unit_test_black(parser_builder_black parser) diff --git a/test/unit/preprocessing/CMakeLists.txt b/test/unit/preprocessing/CMakeLists.txt index 7e142f404..a2381ba90 100644 --- a/test/unit/preprocessing/CMakeLists.txt +++ b/test/unit/preprocessing/CMakeLists.txt @@ -11,4 +11,4 @@ #-----------------------------------------------------------------------------# # Add unit tests -cvc4_add_unit_test_white(pass_bv_gauss_white preprocessing) +cvc4_add_cxx_unit_test_white(pass_bv_gauss_white preprocessing) diff --git a/test/unit/printer/CMakeLists.txt b/test/unit/printer/CMakeLists.txt index 3b040d1fc..93c241af9 100644 --- a/test/unit/printer/CMakeLists.txt +++ b/test/unit/printer/CMakeLists.txt @@ -11,4 +11,4 @@ #-----------------------------------------------------------------------------# # Add unit tests -cvc4_add_unit_test_black(smt2_printer_black printer) +cvc4_add_cxx_unit_test_black(smt2_printer_black printer) diff --git a/test/unit/prop/CMakeLists.txt b/test/unit/prop/CMakeLists.txt index bed0575c6..f866e5ffa 100644 --- a/test/unit/prop/CMakeLists.txt +++ b/test/unit/prop/CMakeLists.txt @@ -11,4 +11,4 @@ #-----------------------------------------------------------------------------# # Add unit tests -cvc4_add_unit_test_white(cnf_stream_white prop) +cvc4_add_cxx_unit_test_white(cnf_stream_white prop) diff --git a/test/unit/test_api.h b/test/unit/test_api.h new file mode 100644 index 000000000..72d0658a7 --- /dev/null +++ b/test/unit/test_api.h @@ -0,0 +1,27 @@ +/********************* */ +/*! \file datatype_api_black.h + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 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 Common header for API unit test. + **/ + +#ifndef CVC4__TEST__UNIT__TEST_API_H +#define CVC4__TEST__UNIT__TEST_API_H + +#include "api/cvc4cpp.h" +#include "gtest/gtest.h" + +class TestApi : public ::testing::Test +{ + protected: + CVC4::api::Solver d_solver; +}; + +#endif diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt index 0eccbf436..334ded2d1 100644 --- a/test/unit/theory/CMakeLists.txt +++ b/test/unit/theory/CMakeLists.txt @@ -8,24 +8,24 @@ ## All rights reserved. See the file COPYING in the top-level source ## directory for licensing information. ## -cvc4_add_unit_test_black(regexp_operation_black theory) -cvc4_add_unit_test_black(theory_black theory) -cvc4_add_unit_test_white(evaluator_white theory) -cvc4_add_unit_test_white(logic_info_white theory) -cvc4_add_unit_test_white(sequences_rewriter_white theory) -cvc4_add_unit_test_white(strings_rewriter_white theory) -cvc4_add_unit_test_white(theory_arith_white theory) -cvc4_add_unit_test_white(theory_bags_normal_form_white theory) -cvc4_add_unit_test_white(theory_bags_rewriter_white theory) -cvc4_add_unit_test_white(theory_bags_type_rules_white theory) -cvc4_add_unit_test_white(theory_bv_rewriter_white theory) -cvc4_add_unit_test_white(theory_bv_white theory) -cvc4_add_unit_test_white(theory_engine_white theory) -cvc4_add_unit_test_white(theory_quantifiers_bv_instantiator_white theory) -cvc4_add_unit_test_white(theory_quantifiers_bv_inverter_white theory) -cvc4_add_unit_test_white(theory_sets_type_enumerator_white theory) -cvc4_add_unit_test_white(theory_sets_type_rules_white theory) -cvc4_add_unit_test_white(theory_strings_skolem_cache_black theory) -cvc4_add_unit_test_white(theory_strings_word_white theory) -cvc4_add_unit_test_white(theory_white theory) -cvc4_add_unit_test_white(type_enumerator_white theory) +cvc4_add_cxx_unit_test_black(regexp_operation_black theory) +cvc4_add_cxx_unit_test_black(theory_black theory) +cvc4_add_cxx_unit_test_white(evaluator_white theory) +cvc4_add_cxx_unit_test_white(logic_info_white theory) +cvc4_add_cxx_unit_test_white(sequences_rewriter_white theory) +cvc4_add_cxx_unit_test_white(strings_rewriter_white theory) +cvc4_add_cxx_unit_test_white(theory_arith_white theory) +cvc4_add_cxx_unit_test_white(theory_bags_normal_form_white theory) +cvc4_add_cxx_unit_test_white(theory_bags_rewriter_white theory) +cvc4_add_cxx_unit_test_white(theory_bags_type_rules_white theory) +cvc4_add_cxx_unit_test_white(theory_bv_rewriter_white theory) +cvc4_add_cxx_unit_test_white(theory_bv_white theory) +cvc4_add_cxx_unit_test_white(theory_engine_white theory) +cvc4_add_cxx_unit_test_white(theory_quantifiers_bv_instantiator_white theory) +cvc4_add_cxx_unit_test_white(theory_quantifiers_bv_inverter_white theory) +cvc4_add_cxx_unit_test_white(theory_sets_type_enumerator_white theory) +cvc4_add_cxx_unit_test_white(theory_sets_type_rules_white theory) +cvc4_add_cxx_unit_test_white(theory_strings_skolem_cache_black theory) +cvc4_add_cxx_unit_test_white(theory_strings_word_white theory) +cvc4_add_cxx_unit_test_white(theory_white theory) +cvc4_add_cxx_unit_test_white(type_enumerator_white theory) diff --git a/test/unit/util/CMakeLists.txt b/test/unit/util/CMakeLists.txt index 0fd7894fe..148ae9910 100644 --- a/test/unit/util/CMakeLists.txt +++ b/test/unit/util/CMakeLists.txt @@ -11,25 +11,25 @@ #-----------------------------------------------------------------------------# # Add unit tests -cvc4_add_unit_test_white(array_store_all_white util) -cvc4_add_unit_test_white(assert_white util) -cvc4_add_unit_test_black(binary_heap_black util) -cvc4_add_unit_test_black(bitvector_black util) -cvc4_add_unit_test_black(boolean_simplification_black util) -cvc4_add_unit_test_black(cardinality_public util) -cvc4_add_unit_test_white(check_white util) -cvc4_add_unit_test_black(configuration_black util) -cvc4_add_unit_test_black(datatype_black util) -cvc4_add_unit_test_black(exception_black util) +cvc4_add_cxx_unit_test_white(array_store_all_white util) +cvc4_add_cxx_unit_test_white(assert_white util) +cvc4_add_cxx_unit_test_black(binary_heap_black util) +cvc4_add_cxx_unit_test_black(bitvector_black util) +cvc4_add_cxx_unit_test_black(boolean_simplification_black util) +cvc4_add_cxx_unit_test_black(cardinality_public util) +cvc4_add_cxx_unit_test_white(check_white util) +cvc4_add_cxx_unit_test_black(configuration_black util) +cvc4_add_cxx_unit_test_black(datatype_black util) +cvc4_add_cxx_unit_test_black(exception_black util) if(CVC4_USE_SYMFPU) -cvc4_add_unit_test_black(floatingpoint_black util) +cvc4_add_cxx_unit_test_black(floatingpoint_black util) endif() -cvc4_add_unit_test_black(integer_black util) -cvc4_add_unit_test_white(integer_white util) -cvc4_add_unit_test_black(output_black util) -cvc4_add_unit_test_black(rational_black util) -cvc4_add_unit_test_white(rational_white util) +cvc4_add_cxx_unit_test_black(integer_black util) +cvc4_add_cxx_unit_test_white(integer_white util) +cvc4_add_cxx_unit_test_black(output_black util) +cvc4_add_cxx_unit_test_black(rational_black util) +cvc4_add_cxx_unit_test_white(rational_white util) if(CVC4_USE_POLY_IMP) -cvc4_add_unit_test_black(real_algebraic_number_black util) +cvc4_add_cxx_unit_test_black(real_algebraic_number_black util) endif() -cvc4_add_unit_test_black(stats_black util) +cvc4_add_cxx_unit_test_black(stats_black util) -- cgit v1.2.3 From fc92c8a035b43733ba50b7672ae40e97dcd9e518 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 1 Dec 2020 19:12:01 -0600 Subject: Remove assertion related to CEGQI dependency lemmas (#5559) This assertion does not hold when we mix --sygus-inst with normal CEGQI. Should fix the nightlies. --- src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index 1a67a2b16..1d917b8f4 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -156,7 +156,11 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q) { d_parent_quant[q].push_back(qi); d_children_quant[qi].push_back(q); - Assert(hasAddedCbqiLemma(qi)); + // may not have added the CEX lemma, but the literal is created by + // the following call regardless. One rare case where this can happen + // is if both sygus-inst and CEGQI are being run in parallel, and + // a parent quantified formula is not handled by CEGQI, but a child + // is. Node qicel = getCounterexampleLiteral(qi); dep.push_back(qi); dep.push_back(qicel); @@ -164,6 +168,9 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q) } if (!dep.empty()) { + // This lemma states that if the child is active, then the parent must + // be asserted, in particular G => Q where G is the CEX literal for the + // child and Q is the parent. Node dep_lemma = nm->mkNode(IMPLIES, ceLit, nm->mkNode(AND, dep)); Trace("cegqi-lemma") << "Counterexample dependency lemma : " << dep_lemma << std::endl; -- cgit v1.2.3 From f79539e2576ae0c38359389dc5b693090acdf56b Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Tue, 1 Dec 2020 18:05:27 -0800 Subject: Remove use of this-> in FP literal. (#5565) --- src/util/floatingpoint_literal_symfpu.cpp | 78 +++++++++++++++--------------- src/util/floatingpoint_literal_symfpu.h.in | 7 ++- 2 files changed, 45 insertions(+), 40 deletions(-) diff --git a/src/util/floatingpoint_literal_symfpu.cpp b/src/util/floatingpoint_literal_symfpu.cpp index fb5c0b7b5..77ab910fa 100644 --- a/src/util/floatingpoint_literal_symfpu.cpp +++ b/src/util/floatingpoint_literal_symfpu.cpp @@ -65,12 +65,12 @@ wrappedBitVector wrappedBitVector::allOnes( template CVC4Prop wrappedBitVector::isAllOnes() const { - return (*this == wrappedBitVector::allOnes(this->getWidth())); + return (*this == wrappedBitVector::allOnes(getWidth())); } template CVC4Prop wrappedBitVector::isAllZeros() const { - return (*this == wrappedBitVector::zero(this->getWidth())); + return (*this == wrappedBitVector::zero(getWidth())); } template @@ -110,101 +110,101 @@ template wrappedBitVector wrappedBitVector::operator<<( const wrappedBitVector& op) const { - return this->BitVector::leftShift(op); + return BitVector::leftShift(op); } template <> wrappedBitVector wrappedBitVector::operator>>( const wrappedBitVector& op) const { - return this->BitVector::arithRightShift(op); + return BitVector::arithRightShift(op); } template <> wrappedBitVector wrappedBitVector::operator>>( const wrappedBitVector& op) const { - return this->BitVector::logicalRightShift(op); + return BitVector::logicalRightShift(op); } template wrappedBitVector wrappedBitVector::operator|( const wrappedBitVector& op) const { - return this->BitVector::operator|(op); + return BitVector::operator|(op); } template wrappedBitVector wrappedBitVector::operator&( const wrappedBitVector& op) const { - return this->BitVector::operator&(op); + return BitVector::operator&(op); } template wrappedBitVector wrappedBitVector::operator+( const wrappedBitVector& op) const { - return this->BitVector::operator+(op); + return BitVector::operator+(op); } template wrappedBitVector wrappedBitVector::operator-( const wrappedBitVector& op) const { - return this->BitVector::operator-(op); + return BitVector::operator-(op); } template wrappedBitVector wrappedBitVector::operator*( const wrappedBitVector& op) const { - return this->BitVector::operator*(op); + return BitVector::operator*(op); } template <> wrappedBitVector wrappedBitVector::operator/( const wrappedBitVector& op) const { - return this->BitVector::unsignedDivTotal(op); + return BitVector::unsignedDivTotal(op); } template <> wrappedBitVector wrappedBitVector::operator%( const wrappedBitVector& op) const { - return this->BitVector::unsignedRemTotal(op); + return BitVector::unsignedRemTotal(op); } template wrappedBitVector wrappedBitVector::operator-(void) const { - return this->BitVector::operator-(); + return BitVector::operator-(); } template wrappedBitVector wrappedBitVector::operator~(void) const { - return this->BitVector::operator~(); + return BitVector::operator~(); } template wrappedBitVector wrappedBitVector::increment() const { - return *this + wrappedBitVector::one(this->getWidth()); + return *this + wrappedBitVector::one(getWidth()); } template wrappedBitVector wrappedBitVector::decrement() const { - return *this - wrappedBitVector::one(this->getWidth()); + return *this - wrappedBitVector::one(getWidth()); } template wrappedBitVector wrappedBitVector::signExtendRightShift( const wrappedBitVector& op) const { - return this->BitVector::arithRightShift(BitVector(this->getWidth(), op)); + return BitVector::arithRightShift(BitVector(getWidth(), op)); } /*** Modular opertaions ***/ @@ -226,13 +226,13 @@ wrappedBitVector wrappedBitVector::modularRightShift( template wrappedBitVector wrappedBitVector::modularIncrement() const { - return this->increment(); + return increment(); } template wrappedBitVector wrappedBitVector::modularDecrement() const { - return this->decrement(); + return decrement(); } template @@ -254,63 +254,63 @@ template CVC4Prop wrappedBitVector::operator==( const wrappedBitVector& op) const { - return this->BitVector::operator==(op); + return BitVector::operator==(op); } template <> CVC4Prop wrappedBitVector::operator<=( const wrappedBitVector& op) const { - return this->signedLessThanEq(op); + return signedLessThanEq(op); } template <> CVC4Prop wrappedBitVector::operator>=( const wrappedBitVector& op) const { - return !(this->signedLessThan(op)); + return !(signedLessThan(op)); } template <> CVC4Prop wrappedBitVector::operator<( const wrappedBitVector& op) const { - return this->signedLessThan(op); + return signedLessThan(op); } template <> CVC4Prop wrappedBitVector::operator>( const wrappedBitVector& op) const { - return !(this->signedLessThanEq(op)); + return !(signedLessThanEq(op)); } template <> CVC4Prop wrappedBitVector::operator<=( const wrappedBitVector& op) const { - return this->unsignedLessThanEq(op); + return unsignedLessThanEq(op); } template <> CVC4Prop wrappedBitVector::operator>=( const wrappedBitVector& op) const { - return !(this->unsignedLessThan(op)); + return !(unsignedLessThan(op)); } template <> CVC4Prop wrappedBitVector::operator<( const wrappedBitVector& op) const { - return this->unsignedLessThan(op); + return unsignedLessThan(op); } template <> CVC4Prop wrappedBitVector::operator>( const wrappedBitVector& op) const { - return !(this->unsignedLessThanEq(op)); + return !(unsignedLessThanEq(op)); } /*** Type conversion ***/ @@ -335,11 +335,11 @@ wrappedBitVector wrappedBitVector::extend( { if (isSigned) { - return this->BitVector::signExtend(extension); + return BitVector::signExtend(extension); } else { - return this->BitVector::zeroExtend(extension); + return BitVector::zeroExtend(extension); } } @@ -347,24 +347,24 @@ template wrappedBitVector wrappedBitVector::contract( CVC4BitWidth reduction) const { - Assert(this->getWidth() > reduction); + Assert(getWidth() > reduction); - return this->extract((this->getWidth() - 1) - reduction, 0); + return extract((getWidth() - 1) - reduction, 0); } template wrappedBitVector wrappedBitVector::resize( CVC4BitWidth newSize) const { - CVC4BitWidth width = this->getWidth(); + CVC4BitWidth width = getWidth(); if (newSize > width) { - return this->extend(newSize - width); + return extend(newSize - width); } else if (newSize < width) { - return this->contract(width - newSize); + return contract(width - newSize); } else { @@ -376,15 +376,15 @@ template wrappedBitVector wrappedBitVector::matchWidth( const wrappedBitVector& op) const { - Assert(this->getWidth() <= op.getWidth()); - return this->extend(op.getWidth() - this->getWidth()); + Assert(getWidth() <= op.getWidth()); + return extend(op.getWidth() - getWidth()); } template wrappedBitVector wrappedBitVector::append( const wrappedBitVector& op) const { - return this->BitVector::concat(op); + return BitVector::concat(op); } // Inclusive of end points, thus if the same, extracts just one bit @@ -393,7 +393,7 @@ wrappedBitVector wrappedBitVector::extract( CVC4BitWidth upper, CVC4BitWidth lower) const { Assert(upper >= lower); - return this->BitVector::extract(upper, lower); + return BitVector::extract(upper, lower); } // Explicit instantiation diff --git a/src/util/floatingpoint_literal_symfpu.h.in b/src/util/floatingpoint_literal_symfpu.h.in index 06a98b7ea..54156c7e7 100644 --- a/src/util/floatingpoint_literal_symfpu.h.in +++ b/src/util/floatingpoint_literal_symfpu.h.in @@ -236,25 +236,30 @@ class wrappedBitVector : public BitVector /** Bit-vector signed/unsigned (zero) extension. */ wrappedBitVector extend(CVC4BitWidth extension) const; + /** * Create a "contracted" bit-vector by cutting off the 'reduction' number of * most significant bits, i.e., by extracting the (bit-width - reduction) * least significant bits. */ wrappedBitVector contract(CVC4BitWidth reduction) const; + /** * Create a "resized" bit-vector of given size bei either extending (if new * size is larger) or contracting (if it is smaller) this wrapped bit-vector. */ wrappedBitVector resize(CVC4BitWidth newSize) const; + /** * Create an extension of this bit-vector that matches the bit-width of the * given bit-vector. + * * Note: The size of the given bit-vector may not be larger than the size of - * this bit-vector. + * this bit-vector. */ wrappedBitVector matchWidth( const wrappedBitVector& op) const; + /** Bit-vector concatenation. */ wrappedBitVector append(const wrappedBitVector& op) const; -- cgit v1.2.3 From 558efa2593fda09235c5f2163836771680d3442a Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Tue, 1 Dec 2020 18:24:21 -0800 Subject: google test: api: Migrate result_black. (#5569) google test: api: Migrate result_black. --- test/unit/api/CMakeLists.txt | 2 +- test/unit/api/result_black.cpp | 115 +++++++++++++++++++++++++++++++++++ test/unit/api/result_black.h | 132 ----------------------------------------- 3 files changed, 116 insertions(+), 133 deletions(-) create mode 100644 test/unit/api/result_black.cpp delete mode 100644 test/unit/api/result_black.h diff --git a/test/unit/api/CMakeLists.txt b/test/unit/api/CMakeLists.txt index 9fcf881a8..a8c696c00 100644 --- a/test/unit/api/CMakeLists.txt +++ b/test/unit/api/CMakeLists.txt @@ -13,7 +13,7 @@ cvc4_add_unit_test_black(datatype_api_black api) cvc4_add_cxx_unit_test_black(op_black api) -cvc4_add_cxx_unit_test_black(result_black api) +cvc4_add_unit_test_black(result_black api) cvc4_add_cxx_unit_test_black(solver_black api) cvc4_add_cxx_unit_test_black(sort_black api) cvc4_add_cxx_unit_test_black(term_black api) diff --git a/test/unit/api/result_black.cpp b/test/unit/api/result_black.cpp new file mode 100644 index 000000000..260845495 --- /dev/null +++ b/test/unit/api/result_black.cpp @@ -0,0 +1,115 @@ +/********************* */ +/*! \file result_black.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 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 Black box testing of the Result class + **/ + +#include "test_api.h" + +using namespace CVC4::api; + +class TestApiResultBlack : public TestApi +{ +}; + +TEST_F(TestApiResultBlack, isNull) +{ + Result res_null; + ASSERT_TRUE(res_null.isNull()); + ASSERT_FALSE(res_null.isSat()); + ASSERT_FALSE(res_null.isUnsat()); + ASSERT_FALSE(res_null.isSatUnknown()); + ASSERT_FALSE(res_null.isEntailed()); + ASSERT_FALSE(res_null.isNotEntailed()); + ASSERT_FALSE(res_null.isEntailmentUnknown()); + Sort u_sort = d_solver.mkUninterpretedSort("u"); + Term x = d_solver.mkVar(u_sort, "x"); + d_solver.assertFormula(x.eqTerm(x)); + Result res = d_solver.checkSat(); + ASSERT_FALSE(res.isNull()); +} + +TEST_F(TestApiResultBlack, eq) +{ + Sort u_sort = d_solver.mkUninterpretedSort("u"); + Term x = d_solver.mkVar(u_sort, "x"); + d_solver.assertFormula(x.eqTerm(x)); + Result res; + Result res2 = d_solver.checkSat(); + Result res3 = d_solver.checkSat(); + res = res2; + EXPECT_EQ(res, res2); + EXPECT_EQ(res3, res2); +} + +TEST_F(TestApiResultBlack, isSat) +{ + Sort u_sort = d_solver.mkUninterpretedSort("u"); + Term x = d_solver.mkVar(u_sort, "x"); + d_solver.assertFormula(x.eqTerm(x)); + Result res = d_solver.checkSat(); + ASSERT_TRUE(res.isSat()); + ASSERT_FALSE(res.isSatUnknown()); +} + +TEST_F(TestApiResultBlack, isUnsat) +{ + Sort u_sort = d_solver.mkUninterpretedSort("u"); + Term x = d_solver.mkVar(u_sort, "x"); + d_solver.assertFormula(x.eqTerm(x).notTerm()); + Result res = d_solver.checkSat(); + ASSERT_TRUE(res.isUnsat()); + ASSERT_FALSE(res.isSatUnknown()); +} + +TEST_F(TestApiResultBlack, isSatUnknown) +{ + d_solver.setLogic("QF_NIA"); + d_solver.setOption("incremental", "false"); + d_solver.setOption("solve-int-as-bv", "32"); + Sort int_sort = d_solver.getIntegerSort(); + Term x = d_solver.mkVar(int_sort, "x"); + d_solver.assertFormula(x.eqTerm(x).notTerm()); + Result res = d_solver.checkSat(); + ASSERT_FALSE(res.isSat()); + ASSERT_TRUE(res.isSatUnknown()); +} + +TEST_F(TestApiResultBlack, isEntailed) +{ + d_solver.setOption("incremental", "true"); + Sort u_sort = d_solver.mkUninterpretedSort("u"); + Term x = d_solver.mkConst(u_sort, "x"); + Term y = d_solver.mkConst(u_sort, "y"); + Term a = x.eqTerm(y).notTerm(); + Term b = x.eqTerm(y); + d_solver.assertFormula(a); + Result entailed = d_solver.checkEntailed(a); + ASSERT_TRUE(entailed.isEntailed()); + ASSERT_FALSE(entailed.isEntailmentUnknown()); + Result not_entailed = d_solver.checkEntailed(b); + ASSERT_TRUE(not_entailed.isNotEntailed()); + ASSERT_FALSE(not_entailed.isEntailmentUnknown()); +} + +TEST_F(TestApiResultBlack, isEntailmentUnknown) +{ + d_solver.setLogic("QF_NIA"); + d_solver.setOption("incremental", "false"); + d_solver.setOption("solve-int-as-bv", "32"); + Sort int_sort = d_solver.getIntegerSort(); + Term x = d_solver.mkVar(int_sort, "x"); + d_solver.assertFormula(x.eqTerm(x).notTerm()); + Result res = d_solver.checkEntailed(x.eqTerm(x)); + ASSERT_FALSE(res.isEntailed()); + ASSERT_TRUE(res.isEntailmentUnknown()); + EXPECT_EQ(res.getUnknownExplanation(), "UNKNOWN_REASON"); +} diff --git a/test/unit/api/result_black.h b/test/unit/api/result_black.h deleted file mode 100644 index aaa59e506..000000000 --- a/test/unit/api/result_black.h +++ /dev/null @@ -1,132 +0,0 @@ -/********************* */ -/*! \file result_black.h - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 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 Black box testing of the Result class - **/ - -#include - -#include "api/cvc4cpp.h" - -using namespace CVC4::api; - -class ResultBlack : public CxxTest::TestSuite -{ - public: - void setUp() { d_solver.reset(new Solver()); } - void tearDown() override { d_solver.reset(nullptr); } - - void testIsNull(); - void testEq(); - void testIsSat(); - void testIsUnsat(); - void testIsSatUnknown(); - void testIsEntailed(); - void testIsEntailmentUnknown(); - - private: - std::unique_ptr d_solver; -}; - -void ResultBlack::testIsNull() -{ - Result res_null; - TS_ASSERT(res_null.isNull()); - TS_ASSERT(!res_null.isSat()); - TS_ASSERT(!res_null.isUnsat()); - TS_ASSERT(!res_null.isSatUnknown()); - TS_ASSERT(!res_null.isEntailed()); - TS_ASSERT(!res_null.isNotEntailed()); - TS_ASSERT(!res_null.isEntailmentUnknown()); - Sort u_sort = d_solver->mkUninterpretedSort("u"); - Term x = d_solver->mkVar(u_sort, "x"); - d_solver->assertFormula(x.eqTerm(x)); - Result res = d_solver->checkSat(); - TS_ASSERT(!res.isNull()); -} - -void ResultBlack::testEq() -{ - Sort u_sort = d_solver->mkUninterpretedSort("u"); - Term x = d_solver->mkVar(u_sort, "x"); - d_solver->assertFormula(x.eqTerm(x)); - Result res; - Result res2 = d_solver->checkSat(); - Result res3 = d_solver->checkSat(); - res = res2; - TS_ASSERT_EQUALS(res, res2); - TS_ASSERT_EQUALS(res3, res2); -} - -void ResultBlack::testIsSat() -{ - Sort u_sort = d_solver->mkUninterpretedSort("u"); - Term x = d_solver->mkVar(u_sort, "x"); - d_solver->assertFormula(x.eqTerm(x)); - Result res = d_solver->checkSat(); - TS_ASSERT(res.isSat()); - TS_ASSERT(!res.isSatUnknown()); -} - -void ResultBlack::testIsUnsat() -{ - Sort u_sort = d_solver->mkUninterpretedSort("u"); - Term x = d_solver->mkVar(u_sort, "x"); - d_solver->assertFormula(x.eqTerm(x).notTerm()); - Result res = d_solver->checkSat(); - TS_ASSERT(res.isUnsat()); - TS_ASSERT(!res.isSatUnknown()); -} - -void ResultBlack::testIsSatUnknown() -{ - d_solver->setLogic("QF_NIA"); - d_solver->setOption("incremental", "false"); - d_solver->setOption("solve-int-as-bv", "32"); - Sort int_sort = d_solver->getIntegerSort(); - Term x = d_solver->mkVar(int_sort, "x"); - d_solver->assertFormula(x.eqTerm(x).notTerm()); - Result res = d_solver->checkSat(); - TS_ASSERT(!res.isSat()); - TS_ASSERT(res.isSatUnknown()); -} - -void ResultBlack::testIsEntailed() -{ - d_solver->setOption("incremental", "true"); - Sort u_sort = d_solver->mkUninterpretedSort("u"); - Term x = d_solver->mkConst(u_sort, "x"); - Term y = d_solver->mkConst(u_sort, "y"); - Term a = x.eqTerm(y).notTerm(); - Term b = x.eqTerm(y); - d_solver->assertFormula(a); - Result entailed = d_solver->checkEntailed(a); - TS_ASSERT(entailed.isEntailed()); - TS_ASSERT(!entailed.isEntailmentUnknown()); - Result not_entailed = d_solver->checkEntailed(b); - TS_ASSERT(not_entailed.isNotEntailed()); - TS_ASSERT(!not_entailed.isEntailmentUnknown()); -} - -void ResultBlack::testIsEntailmentUnknown() -{ - d_solver->setLogic("QF_NIA"); - d_solver->setOption("incremental", "false"); - d_solver->setOption("solve-int-as-bv", "32"); - Sort int_sort = d_solver->getIntegerSort(); - Term x = d_solver->mkVar(int_sort, "x"); - d_solver->assertFormula(x.eqTerm(x).notTerm()); - Result res = d_solver->checkEntailed(x.eqTerm(x)); - TS_ASSERT(!res.isEntailed()); - TS_ASSERT(res.isEntailmentUnknown()); - TS_ASSERT_EQUALS(res.getUnknownExplanation(), "UNKNOWN_REASON"); -} - -- cgit v1.2.3 From 901cea314c4dc3be411c345e42c858063fe5aa1b Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 2 Dec 2020 06:22:56 +0100 Subject: Add regressions from #3687. (#5553) The error from #3687 has been fixed in the meantime. This PR adds the two examples from this issue as regressions. Closes #3687 --- test/regress/CMakeLists.txt | 2 + .../aufbv/issue3687-check-models-small.smt2 | 8 ++++ test/regress/regress2/issue3687-check-models.smt2 | 51 ++++++++++++++++++++++ 3 files changed, 61 insertions(+) create mode 100644 test/regress/regress0/aufbv/issue3687-check-models-small.smt2 create mode 100644 test/regress/regress2/issue3687-check-models.smt2 diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index fda5c69eb..1826b3156 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -126,6 +126,7 @@ set(regress_0_tests regress0/aufbv/fuzz14.smtv1.smt2 regress0/aufbv/fuzz15.smtv1.smt2 regress0/aufbv/issue3737.smt2 + regress0/aufbv/issue3687-check-models-small.smt2 regress0/aufbv/rewrite_bug.smtv1.smt2 regress0/aufbv/try3_sameret_functions_fse-bfs_tac.calc_next.il.fse-bfs.delta01.smtv1.smt2 regress0/aufbv/try5_small_difret_functions_wp_su.set_char_quoting.il.wp.delta01.smtv1.smt2 @@ -2176,6 +2177,7 @@ set(regress_2_tests regress2/hole7.cvc regress2/hole8.cvc regress2/instance_1444.smtv1.smt2 + regress2/issue3687-check-models.smt2 regress2/issue4707-bv-to-bool-large.smt2 regress2/javafe.ast.StandardPrettyPrint.319_no_forall.smt2 regress2/javafe.ast.WhileStmt.447_no_forall.smt2 diff --git a/test/regress/regress0/aufbv/issue3687-check-models-small.smt2 b/test/regress/regress0/aufbv/issue3687-check-models-small.smt2 new file mode 100644 index 000000000..88cbd8a0b --- /dev/null +++ b/test/regress/regress0/aufbv/issue3687-check-models-small.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --check-models +; EXPECT: sat +(set-logic QF_AUFBV) +(declare-fun a () (Array (_ BitVec 2) (_ BitVec 2))) +(declare-fun b () (_ BitVec 2)) +(assert (distinct #b01 (select (store (store a #b01 (bvor #b01 (select a + #b00))) #b10 #b00) b))) +(check-sat) \ No newline at end of file diff --git a/test/regress/regress2/issue3687-check-models.smt2 b/test/regress/regress2/issue3687-check-models.smt2 new file mode 100644 index 000000000..02f7754cf --- /dev/null +++ b/test/regress/regress2/issue3687-check-models.smt2 @@ -0,0 +1,51 @@ +; COMMAND-LINE: --check-models +; EXPECT: sat +(set-logic QF_ABV) +(declare-fun c () (_ BitVec 32)) +(declare-fun a () (Array (_ BitVec 32) (_ BitVec 8))) +(declare-fun b () (_ BitVec 32)) +(assert (let ((a!1 (bvxnor (concat #x000000 (select a (bvadd c #x00000001))) #x00000008)) + (a!3 (bvsdiv (concat #x000000 (select a (bvadd c #x00000002))) #x00000010)) + (a!4 (bvudiv (concat #x000000 (select a (bvashr c #x00000003))) + #x00000018)) + (a!5 (select a + (bvxor (bvsub (bvnand c #x00000004) #x00000004) #x00000000))) + (a!6 (select a + (bvsdiv (bvsub (bvnand c #x00000004) #x00000004) #x00000001))) + (a!7 (select a + (bvadd (bvsub (bvnand c #x00000004) #x00000004) #x00000002))) + (a!9 (store a + (bvashr (bvurem (bvnand c #x00000004) #x00000004) #x00000001) + ((_ extract 7 0) (bvxnor b #x00000008)))) + (a!11 (bvnand (bvurem (bvsub (bvnand c #x00000004) #x00000004) #x00000004) + #x00000008))) +(let ((a!2 (bvnor (concat #x000000 (select a (bvsmod c #x00000000))) a!1)) + (a!8 (bvlshr (bvor (concat #x000000 a!5) + (bvmul (concat #x000000 a!6) #x00000008)) + (bvand (concat #x000000 a!7) #x00000010))) + (a!10 (store a!9 + (bvshl (bvurem (bvnand c #x00000004) #x00000004) #x00000000) + ((_ extract 7 0) b))) + (a!12 (bvsub (concat #x000000 (select a (bvashr a!11 #x00000001))) + #x00000008)) + (a!14 (bvxnor (concat #x000000 (select a (bvxnor a!11 #x00000002))) + #x00000010)) + (a!15 (bvxor (concat #x000000 (select a (bvsub a!11 #x00000003))) + #x00000018))) +(let ((a!13 (bvor (concat #x000000 (select a (bvmul a!11 #x00000000))) a!12))) +(let ((a!16 ((_ extract 7 0) + (bvmul (bvurem (bvurem a!13 a!14) a!15) #x00000018))) + (a!17 ((_ extract 7 0) (bvor (bvurem (bvurem a!13 a!14) a!15) #x00000010))) + (a!18 ((_ extract 7 0) + (bvnor (bvurem (bvurem a!13 a!14) a!15) #x00000008)))) +(let ((a!19 (store (store (store (store a!10 #x08053e77 a!16) #x08053e76 a!17) + #x08053e75 + a!18) + #x08053e74 + ((_ extract 7 0) (bvurem (bvurem a!13 a!14) a!15))))) +(let ((a!20 (select a!19 + (bvadd (bvsub (bvnand c #x00000004) #x00000004) #x00000003)))) +(let ((a!21 (distinct (bvsdiv (bvsmod a!2 a!3) a!4) + (bvshl a!8 (bvshl (concat #x000000 a!20) #x00000018))))) + (= #b1 (bvashr (ite (or a!21) #b1 #b0) #b1)))))))))) +(check-sat) -- cgit v1.2.3