From 588fb874c95005f1d379073a750b88a6ba5ee89a Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 14 Oct 2021 08:50:36 -0700 Subject: Fix GLPK linking (#7357) While #7341 added cmake-3.9 compatible linking for GLPK, it did not actually remove the line that triggers the error on older cmake versions. This commit does. --- src/CMakeLists.txt | 1 - 1 file changed, 1 deletion(-) (limited to 'src') diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 733186d16..31dccdbc6 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -1402,7 +1402,6 @@ if(USE_GLPK) if(ENABLE_STATIC_LIBRARY) target_link_libraries(cvc5-static PUBLIC ${GLPK_LIBRARIES}) endif() - target_link_libraries(cvc5-obj PUBLIC ${GLPK_LIBRARIES}) endif() if(USE_POLY) add_dependencies(cvc5-obj Polyxx_SHARED) -- cgit v1.2.3 From 861dba0caea6c8bfa54bca58749323c4dbcfb282 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 14 Oct 2021 11:14:02 -0500 Subject: Fix quantifiers variable elimination for parametric datatypes (#7358) Fixes #7353. --- src/theory/quantifiers/quantifiers_rewriter.cpp | 20 +++++++++++++++++--- test/regress/CMakeLists.txt | 1 + .../quantifiers/issue7353-var-elim-par-dt.smt2 | 9 +++++++++ 3 files changed, 27 insertions(+), 3 deletions(-) create mode 100644 test/regress/regress0/quantifiers/issue7353-var-elim-par-dt.smt2 (limited to 'src') diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 7c7c7aade..52e90e26e 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/quantifiers_rewriter.h" +#include "expr/ascription_type.h" #include "expr/bound_var_manager.h" #include "expr/dtype.h" #include "expr/dtype_cons.h" @@ -895,12 +896,25 @@ bool QuantifiersRewriter::getVarElimLit(Node body, const DType& dt = datatypes::utils::datatypeOf(tester); const DTypeConstructor& c = dt[index]; std::vector newChildren; - newChildren.push_back(c.getConstructor()); + Node cons = c.getConstructor(); + TypeNode tspec; + // take into account if parametric + if (dt.isParametric()) + { + tspec = c.getSpecializedConstructorType(lit[0].getType()); + cons = nm->mkNode( + APPLY_TYPE_ASCRIPTION, nm->mkConst(AscriptionType(tspec)), cons); + } + else + { + tspec = cons.getType(); + } + newChildren.push_back(cons); std::vector newVars; BoundVarManager* bvm = nm->getBoundVarManager(); - for (unsigned j = 0, nargs = c.getNumArgs(); j < nargs; j++) + for (size_t j = 0, nargs = c.getNumArgs(); j < nargs; j++) { - TypeNode tn = c[j].getRangeType(); + TypeNode tn = tspec[j]; Node rn = nm->mkConst(Rational(j)); Node cacheVal = BoundVarManager::getCacheValue(body, lit, rn); Node v = bvm->mkBoundVar(cacheVal, tn); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 907dc22d1..79a493a1f 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -921,6 +921,7 @@ set(regress_0_tests regress0/quantifiers/issue6838-qpdt.smt2 regress0/quantifiers/issue6996-trivial-elim.smt2 regress0/quantifiers/issue6999-deq-elim.smt2 + regress0/quantifiers/issue7353-var-elim-par-dt.smt2 regress0/quantifiers/lra-triv-gn.smt2 regress0/quantifiers/macro-back-subs-sat.smt2 regress0/quantifiers/macros-int-real.smt2 diff --git a/test/regress/regress0/quantifiers/issue7353-var-elim-par-dt.smt2 b/test/regress/regress0/quantifiers/issue7353-var-elim-par-dt.smt2 new file mode 100644 index 000000000..8c9d9eb66 --- /dev/null +++ b/test/regress/regress0/quantifiers/issue7353-var-elim-par-dt.smt2 @@ -0,0 +1,9 @@ +(set-logic ALL) +(set-info :status sat) +(declare-datatype Option (par (T) ((none) (some (extractSome T))))) +(assert + (forall ((x (Option Int))) + (=> (and ((_ is some) x) + (= (extractSome x) 0)) + (= x (some 0))))) +(check-sat) -- cgit v1.2.3 From 5c481b34eef5860d29ea1f2f62cea696fea01619 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 14 Oct 2021 14:15:29 -0500 Subject: Split entailment check from term database (#7342) Towards addressing some bottlenecks on Facebook benchmarks. --- src/CMakeLists.txt | 2 + src/theory/quantifiers/conjecture_generator.cpp | 6 +- src/theory/quantifiers/ematching/ho_trigger.cpp | 4 +- src/theory/quantifiers/entailment_check.cpp | 443 ++++++++++++++++++++++++ src/theory/quantifiers/entailment_check.h | 150 ++++++++ src/theory/quantifiers/instantiate.cpp | 10 +- src/theory/quantifiers/quant_conflict_find.cpp | 30 +- src/theory/quantifiers/term_database.cpp | 360 ------------------- src/theory/quantifiers/term_database.h | 90 ----- src/theory/quantifiers/term_registry.cpp | 7 + src/theory/quantifiers/term_registry.h | 5 + 11 files changed, 632 insertions(+), 475 deletions(-) create mode 100644 src/theory/quantifiers/entailment_check.cpp create mode 100644 src/theory/quantifiers/entailment_check.h (limited to 'src') diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 31dccdbc6..374c57726 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -805,6 +805,8 @@ libcvc5_add_sources( theory/quantifiers/ematching/trigger_trie.h theory/quantifiers/ematching/var_match_generator.cpp theory/quantifiers/ematching/var_match_generator.h + theory/quantifiers/entailment_check.cpp + theory/quantifiers/entailment_check.h theory/quantifiers/equality_query.cpp theory/quantifiers/equality_query.h theory/quantifiers/expr_miner.cpp diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index b98088a71..d778a679e 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -245,6 +245,7 @@ Node ConjectureGenerator::getUniversalRepresentative(TNode n, bool add) // now, do instantiation-based merging for each of these terms Trace("thm-ee-debug") << "Merge equivalence classes based on instantiations of terms..." << std::endl; //merge all pending equalities + EntailmentCheck* echeck = d_treg.getEntailmentCheck(); while( !d_upendingAdds.empty() ){ Trace("sg-pending") << "Add " << d_upendingAdds.size() << " pending terms..." << std::endl; std::vector< Node > pending; @@ -256,7 +257,7 @@ Node ConjectureGenerator::getUniversalRepresentative(TNode n, bool add) Trace("thm-ee-add") << "UEE : Add universal term " << t << std::endl; std::vector< Node > eq_terms; //if occurs modulo equality at ground level, it is equivalent to representative of ground equality engine - Node gt = getTermDatabase()->evaluateTerm(t); + Node gt = echeck->evaluateTerm(t); if( !gt.isNull() && gt!=t ){ eq_terms.push_back( gt ); } @@ -1362,7 +1363,8 @@ bool ConjectureGenerator::notifySubstitution( TNode glhs, std::map< TNode, TNode } Trace("sg-cconj-debug") << "Evaluate RHS : : " << rhs << std::endl; //get the representative of rhs with substitution subs - TNode grhs = getTermDatabase()->getEntailedTerm( rhs, subs, true ); + EntailmentCheck* echeck = d_treg.getEntailmentCheck(); + TNode grhs = echeck->getEntailedTerm(rhs, subs, true); Trace("sg-cconj-debug") << "...done evaluating term, got : " << grhs << std::endl; if( !grhs.isNull() ){ if( glhs!=grhs ){ diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp index a8ab760ce..d2b0b0542 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.cpp +++ b/src/theory/quantifiers/ematching/ho_trigger.cpp @@ -238,6 +238,7 @@ bool HigherOrderTrigger::sendInstantiation(std::vector& m, InferenceId id) d_lchildren.clear(); d_arg_to_arg_rep.clear(); d_arg_vector.clear(); + EntailmentCheck* echeck = d_treg.getEntailmentCheck(); for (std::pair >& ha : ho_var_apps_subs) { TNode var = ha.first; @@ -291,8 +292,7 @@ bool HigherOrderTrigger::sendInstantiation(std::vector& m, InferenceId id) { if (!d_qstate.areEqual(itf->second, args[k])) { - if (!d_treg.getTermDatabase()->isEntailed( - itf->second.eqNode(args[k]), true)) + if (!echeck->isEntailed(itf->second.eqNode(args[k]), true)) { fixed_vals[k] = Node::null(); } diff --git a/src/theory/quantifiers/entailment_check.cpp b/src/theory/quantifiers/entailment_check.cpp new file mode 100644 index 000000000..f27e14121 --- /dev/null +++ b/src/theory/quantifiers/entailment_check.cpp @@ -0,0 +1,443 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Implementation of entailment check class. + */ + +#include "theory/quantifiers/entailment_check.h" + +#include "theory/quantifiers/quantifiers_state.h" +#include "theory/quantifiers/term_database.h" + +using namespace cvc5::kind; +using namespace cvc5::context; + +namespace cvc5 { +namespace theory { +namespace quantifiers { + +EntailmentCheck::EntailmentCheck(Env& env, QuantifiersState& qs, TermDb& tdb) + : EnvObj(env), d_qstate(qs), d_tdb(tdb) +{ + d_true = NodeManager::currentNM()->mkConst(true); + d_false = NodeManager::currentNM()->mkConst(false); +} + +EntailmentCheck::~EntailmentCheck() {} +Node EntailmentCheck::evaluateTerm2(TNode n, + std::map& visited, + std::vector& exp, + bool useEntailmentTests, + bool computeExp, + bool reqHasTerm) +{ + std::map::iterator itv = visited.find(n); + if (itv != visited.end()) + { + return itv->second; + } + size_t prevSize = exp.size(); + Trace("term-db-eval") << "evaluate term : " << n << std::endl; + Node ret = n; + if (n.getKind() == FORALL || n.getKind() == BOUND_VARIABLE) + { + // do nothing + } + else if (d_qstate.hasTerm(n)) + { + Trace("term-db-eval") << "...exists in ee, return rep" << std::endl; + ret = d_qstate.getRepresentative(n); + if (computeExp) + { + if (n != ret) + { + exp.push_back(n.eqNode(ret)); + } + } + reqHasTerm = false; + } + else if (n.hasOperator()) + { + std::vector args; + bool ret_set = false; + Kind k = n.getKind(); + std::vector tempExp; + for (unsigned i = 0, nchild = n.getNumChildren(); i < nchild; i++) + { + TNode c = evaluateTerm2( + n[i], visited, tempExp, useEntailmentTests, computeExp, reqHasTerm); + if (c.isNull()) + { + ret = Node::null(); + ret_set = true; + break; + } + else if (c == d_true || c == d_false) + { + // short-circuiting + if ((k == AND && c == d_false) || (k == OR && c == d_true)) + { + ret = c; + ret_set = true; + reqHasTerm = false; + break; + } + else if (k == ITE && i == 0) + { + ret = evaluateTerm2(n[c == d_true ? 1 : 2], + visited, + tempExp, + useEntailmentTests, + computeExp, + reqHasTerm); + ret_set = true; + reqHasTerm = false; + break; + } + } + if (computeExp) + { + exp.insert(exp.end(), tempExp.begin(), tempExp.end()); + } + Trace("term-db-eval") << " child " << i << " : " << c << std::endl; + args.push_back(c); + } + if (ret_set) + { + // if we short circuited + if (computeExp) + { + exp.clear(); + exp.insert(exp.end(), tempExp.begin(), tempExp.end()); + } + } + else + { + // get the (indexed) operator of n, if it exists + TNode f = d_tdb.getMatchOperator(n); + // if it is an indexed term, return the congruent term + if (!f.isNull()) + { + // if f is congruent to a term indexed by this class + TNode nn = d_tdb.getCongruentTerm(f, args); + Trace("term-db-eval") << " got congruent term " << nn + << " from DB for " << n << std::endl; + if (!nn.isNull()) + { + if (computeExp) + { + Assert(nn.getNumChildren() == n.getNumChildren()); + for (size_t i = 0, nchild = nn.getNumChildren(); i < nchild; i++) + { + if (nn[i] != n[i]) + { + exp.push_back(nn[i].eqNode(n[i])); + } + } + } + ret = d_qstate.getRepresentative(nn); + Trace("term-db-eval") << "return rep" << std::endl; + ret_set = true; + reqHasTerm = false; + Assert(!ret.isNull()); + if (computeExp) + { + if (n != ret) + { + exp.push_back(nn.eqNode(ret)); + } + } + } + } + if (!ret_set) + { + Trace("term-db-eval") << "return rewrite" << std::endl; + // a theory symbol or a new UF term + if (n.getMetaKind() == metakind::PARAMETERIZED) + { + args.insert(args.begin(), n.getOperator()); + } + ret = NodeManager::currentNM()->mkNode(n.getKind(), args); + ret = rewrite(ret); + if (ret.getKind() == EQUAL) + { + if (d_qstate.areDisequal(ret[0], ret[1])) + { + ret = d_false; + } + } + if (useEntailmentTests) + { + if (ret.getKind() == EQUAL || ret.getKind() == GEQ) + { + Valuation& val = d_qstate.getValuation(); + for (unsigned j = 0; j < 2; j++) + { + std::pair et = val.entailmentCheck( + options::TheoryOfMode::THEORY_OF_TYPE_BASED, + j == 0 ? ret : ret.negate()); + if (et.first) + { + ret = j == 0 ? d_true : d_false; + if (computeExp) + { + exp.push_back(et.second); + } + break; + } + } + } + } + } + } + } + // must have the term + if (reqHasTerm && !ret.isNull()) + { + Kind k = ret.getKind(); + if (k != OR && k != AND && k != EQUAL && k != ITE && k != NOT + && k != FORALL) + { + if (!d_qstate.hasTerm(ret)) + { + ret = Node::null(); + } + } + } + Trace("term-db-eval") << "evaluated term : " << n << ", got : " << ret + << ", reqHasTerm = " << reqHasTerm << std::endl; + // clear the explanation if failed + if (computeExp && ret.isNull()) + { + exp.resize(prevSize); + } + visited[n] = ret; + return ret; +} + +TNode EntailmentCheck::getEntailedTerm2(TNode n, + std::map& subs, + bool subsRep, + bool hasSubs) +{ + Trace("term-db-entail") << "get entailed term : " << n << std::endl; + if (d_qstate.hasTerm(n)) + { + Trace("term-db-entail") << "...exists in ee, return rep " << std::endl; + return n; + } + else if (n.getKind() == BOUND_VARIABLE) + { + if (hasSubs) + { + std::map::iterator it = subs.find(n); + if (it != subs.end()) + { + Trace("term-db-entail") + << "...substitution is : " << it->second << std::endl; + if (subsRep) + { + Assert(d_qstate.hasTerm(it->second)); + Assert(d_qstate.getRepresentative(it->second) == it->second); + return it->second; + } + return getEntailedTerm2(it->second, subs, subsRep, hasSubs); + } + } + } + else if (n.getKind() == ITE) + { + for (uint32_t i = 0; i < 2; i++) + { + if (isEntailed2(n[0], subs, subsRep, hasSubs, i == 0)) + { + return getEntailedTerm2(n[i == 0 ? 1 : 2], subs, subsRep, hasSubs); + } + } + } + else + { + if (n.hasOperator()) + { + TNode f = d_tdb.getMatchOperator(n); + if (!f.isNull()) + { + std::vector args; + for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++) + { + TNode c = getEntailedTerm2(n[i], subs, subsRep, hasSubs); + if (c.isNull()) + { + return TNode::null(); + } + c = d_qstate.getRepresentative(c); + Trace("term-db-entail") << " child " << i << " : " << c << std::endl; + args.push_back(c); + } + TNode nn = d_tdb.getCongruentTerm(f, args); + Trace("term-db-entail") + << " got congruent term " << nn << " for " << n << std::endl; + return nn; + } + } + } + return TNode::null(); +} + +Node EntailmentCheck::evaluateTerm(TNode n, + bool useEntailmentTests, + bool reqHasTerm) +{ + std::map visited; + std::vector exp; + return evaluateTerm2(n, visited, exp, useEntailmentTests, false, reqHasTerm); +} + +Node EntailmentCheck::evaluateTerm(TNode n, + std::vector& exp, + bool useEntailmentTests, + bool reqHasTerm) +{ + std::map visited; + return evaluateTerm2(n, visited, exp, useEntailmentTests, true, reqHasTerm); +} + +TNode EntailmentCheck::getEntailedTerm(TNode n, + std::map& subs, + bool subsRep) +{ + return getEntailedTerm2(n, subs, subsRep, true); +} + +TNode EntailmentCheck::getEntailedTerm(TNode n) +{ + std::map subs; + return getEntailedTerm2(n, subs, false, false); +} + +bool EntailmentCheck::isEntailed2( + TNode n, std::map& subs, bool subsRep, bool hasSubs, bool pol) +{ + Trace("term-db-entail") << "Check entailed : " << n << ", pol = " << pol + << std::endl; + Assert(n.getType().isBoolean()); + if (n.getKind() == EQUAL && !n[0].getType().isBoolean()) + { + TNode n1 = getEntailedTerm2(n[0], subs, subsRep, hasSubs); + if (!n1.isNull()) + { + TNode n2 = getEntailedTerm2(n[1], subs, subsRep, hasSubs); + if (!n2.isNull()) + { + if (n1 == n2) + { + return pol; + } + else + { + Assert(d_qstate.hasTerm(n1)); + Assert(d_qstate.hasTerm(n2)); + if (pol) + { + return d_qstate.areEqual(n1, n2); + } + else + { + return d_qstate.areDisequal(n1, n2); + } + } + } + } + } + else if (n.getKind() == NOT) + { + return isEntailed2(n[0], subs, subsRep, hasSubs, !pol); + } + else if (n.getKind() == OR || n.getKind() == AND) + { + bool simPol = (pol && n.getKind() == OR) || (!pol && n.getKind() == AND); + for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++) + { + if (isEntailed2(n[i], subs, subsRep, hasSubs, pol)) + { + if (simPol) + { + return true; + } + } + else + { + if (!simPol) + { + return false; + } + } + } + return !simPol; + // Boolean equality here + } + else if (n.getKind() == EQUAL || n.getKind() == ITE) + { + for (size_t i = 0; i < 2; i++) + { + if (isEntailed2(n[0], subs, subsRep, hasSubs, i == 0)) + { + size_t ch = (n.getKind() == EQUAL || i == 0) ? 1 : 2; + bool reqPol = (n.getKind() == ITE || i == 0) ? pol : !pol; + return isEntailed2(n[ch], subs, subsRep, hasSubs, reqPol); + } + } + } + else if (n.getKind() == APPLY_UF) + { + TNode n1 = getEntailedTerm2(n, subs, subsRep, hasSubs); + if (!n1.isNull()) + { + Assert(d_qstate.hasTerm(n1)); + if (n1 == d_true) + { + return pol; + } + else if (n1 == d_false) + { + return !pol; + } + else + { + return d_qstate.getRepresentative(n1) == (pol ? d_true : d_false); + } + } + } + else if (n.getKind() == FORALL && !pol) + { + return isEntailed2(n[1], subs, subsRep, hasSubs, pol); + } + return false; +} + +bool EntailmentCheck::isEntailed(TNode n, bool pol) +{ + std::map subs; + return isEntailed2(n, subs, false, false, pol); +} + +bool EntailmentCheck::isEntailed(TNode n, + std::map& subs, + bool subsRep, + bool pol) +{ + return isEntailed2(n, subs, subsRep, true, pol); +} + +} // namespace quantifiers +} // namespace theory +} // namespace cvc5 diff --git a/src/theory/quantifiers/entailment_check.h b/src/theory/quantifiers/entailment_check.h new file mode 100644 index 000000000..5f0af60a6 --- /dev/null +++ b/src/theory/quantifiers/entailment_check.h @@ -0,0 +1,150 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Entailment check class + */ + +#include "cvc5_private.h" + +#ifndef CVC5__THEORY__QUANTIFIERS__ENTAILMENT_CHECK_H +#define CVC5__THEORY__QUANTIFIERS__ENTAILMENT_CHECK_H + +#include +#include + +#include "expr/node.h" +#include "smt/env_obj.h" + +namespace cvc5 { +namespace theory { +namespace quantifiers { + +class QuantifiersState; +class TermDb; + +/** + * Entailment check utility, which determines whether formulas are entailed + * in the current context. The main focus of this class is on UF formulas. + * It works by looking at the term argument trie data structures in term + * database. For details, see e.g. Section 4.1 of Reynolds et al TACAS 2018. + */ +class EntailmentCheck : protected EnvObj +{ + public: + EntailmentCheck(Env& env, QuantifiersState& qs, TermDb& tdb); + ~EntailmentCheck(); + /** evaluate term + * + * Returns a term n' such that n = n' is entailed based on the equality + * information ee. This function may generate new terms. In particular, + * we typically rewrite subterms of n of maximal size to terms that exist in + * the equality engine specified by ee. + * + * useEntailmentTests is whether to call the theory engine's entailmentTest + * on literals n for which this call fails to find a term n' that is + * equivalent to n, for increased precision. This is not frequently used. + * + * The vector exp stores the explanation for why n evaluates to that term, + * that is, if this call returns a non-null node n', then: + * exp => n = n' + * + * If reqHasTerm, then we require that the returned term is a Boolean + * combination of terms that exist in the equality engine used by this call. + * If no such term is constructable, this call returns null. The motivation + * for setting this to true is to "fail fast" if we require the return value + * of this function to only involve existing terms. This is used e.g. in + * the "propagating instances" portion of conflict-based instantiation + * (quant_conflict_find.h). + */ + Node evaluateTerm(TNode n, + std::vector& exp, + bool useEntailmentTests = false, + bool reqHasTerm = false); + /** same as above, without exp */ + Node evaluateTerm(TNode n, + bool useEntailmentTests = false, + bool reqHasTerm = false); + /** get entailed term + * + * If possible, returns a term n' such that: + * (1) n' exists in the current equality engine (as specified by the state), + * (2) n = n' is entailed in the current context. + * It returns null if no such term can be found. + * Wrt evaluateTerm, this version does not construct new terms, and + * thus is less aggressive. + */ + TNode getEntailedTerm(TNode n); + /** get entailed term + * + * If possible, returns a term n' such that: + * (1) n' exists in the current equality engine (as specified by the state), + * (2) n * subs = n' is entailed in the current context, where * denotes + * substitution application. + * It returns null if no such term can be found. + * subsRep is whether the substitution maps to terms that are representatives + * according to the quantifiers state. + * Wrt evaluateTerm, this version does not construct new terms, and + * thus is less aggressive. + */ + TNode getEntailedTerm(TNode n, std::map& subs, bool subsRep); + /** is entailed + * Checks whether the current context entails n with polarity pol, based on + * the equality information in the quantifiers state. Returns true if the + * entailment can be successfully shown. + */ + bool isEntailed(TNode n, bool pol); + /** is entailed + * + * Checks whether the current context entails ( n * subs ) with polarity pol, + * based on the equality information in the quantifiers state, + * where * denotes substitution application. + * subsRep is whether the substitution maps to terms that are representatives + * according to in the quantifiers state. + */ + bool isEntailed(TNode n, + std::map& subs, + bool subsRep, + bool pol); + + protected: + /** helper for evaluate term */ + Node evaluateTerm2(TNode n, + std::map& visited, + std::vector& exp, + bool useEntailmentTests, + bool computeExp, + bool reqHasTerm); + /** helper for get entailed term */ + TNode getEntailedTerm2(TNode n, + std::map& subs, + bool subsRep, + bool hasSubs); + /** helper for is entailed */ + bool isEntailed2(TNode n, + std::map& subs, + bool subsRep, + bool hasSubs, + bool pol); + /** The quantifiers state object */ + QuantifiersState& d_qstate; + /** Reference to the term database */ + TermDb& d_tdb; + /** boolean terms */ + Node d_true; + Node d_false; +}; /* class EntailmentCheck */ + +} // namespace quantifiers +} // namespace theory +} // namespace cvc5 + +#endif /* CVC5__THEORY__QUANTIFIERS__ENTAILMENT_CHECK_H */ diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index f756fcfd1..be04f9404 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -25,6 +25,7 @@ #include "smt/logic_exception.h" #include "smt/smt_statistics_registry.h" #include "theory/quantifiers/cegqi/inst_strategy_cegqi.h" +#include "theory/quantifiers/entailment_check.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_preprocess.h" @@ -183,7 +184,7 @@ bool Instantiate::addInstantiation(Node q, #endif } - TermDb* tdb = d_treg.getTermDatabase(); + EntailmentCheck* ec = d_treg.getEntailmentCheck(); // Note we check for entailment before checking for term vector duplication. // Although checking for term vector duplication is a faster check, it is // included automatically with recordInstantiationInternal, hence we prefer @@ -206,7 +207,7 @@ bool Instantiate::addInstantiation(Node q, { subs[q[0][i]] = terms[i]; } - if (tdb->isEntailed(q[1], subs, false, true)) + if (ec->isEntailed(q[1], subs, false, true)) { Trace("inst-add-debug") << " --> Currently entailed." << std::endl; ++(d_statistics.d_inst_duplicate_ent); @@ -217,6 +218,7 @@ bool Instantiate::addInstantiation(Node q, // check based on instantiation level if (options::instMaxLevel() != -1) { + TermDb* tdb = d_treg.getTermDatabase(); for (Node& t : terms) { if (!tdb->isTermEligibleForInstantiation(t, q)) @@ -409,7 +411,7 @@ bool Instantiate::addInstantiationExpFail(Node q, // will never succeed with 1 variable return false; } - TermDb* tdb = d_treg.getTermDatabase(); + EntailmentCheck* echeck = d_treg.getEntailmentCheck(); Trace("inst-exp-fail") << "Explain inst failure..." << terms << std::endl; // set up information for below std::vector& vars = d_qreg.d_vars[q]; @@ -445,7 +447,7 @@ bool Instantiate::addInstantiationExpFail(Node q, if (options::instNoEntail()) { Trace("inst-exp-fail") << " check entailment" << std::endl; - success = tdb->isEntailed(q[1], subs, false, true); + success = echeck->isEntailed(q[1], subs, false, true); Trace("inst-exp-fail") << " entailed: " << success << std::endl; } // check whether the instantiation rewrites to the same thing diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 361adfd54..dc1043d28 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -577,6 +577,7 @@ bool QuantInfo::isTConstraintSpurious(QuantConflictFind* p, { if( options::qcfEagerTest() ){ //check whether the instantiation evaluates as expected + EntailmentCheck* echeck = p->getTermRegistry().getEntailmentCheck(); if (p->atConflictEffort()) { Trace("qcf-instance-check") << "Possible conflict instance for " << d_q << " : " << std::endl; std::map< TNode, TNode > subs; @@ -584,13 +585,12 @@ bool QuantInfo::isTConstraintSpurious(QuantConflictFind* p, Trace("qcf-instance-check") << " " << terms[i] << std::endl; subs[d_q[0][i]] = terms[i]; } - TermDb* tdb = p->getTermDatabase(); for( unsigned i=0; i " << n << std::endl; subs[d_extra_var[i]] = n; } - if (!tdb->isEntailed(d_q[1], subs, false, false)) + if (!echeck->isEntailed(d_q[1], subs, false, false)) { Trace("qcf-instance-check") << "...not entailed to be false." << std::endl; return true; @@ -599,8 +599,8 @@ bool QuantInfo::isTConstraintSpurious(QuantConflictFind* p, Node inst = getInferenceManager().getInstantiate()->getInstantiation(d_q, terms); inst = Rewriter::rewrite(inst); - Node inst_eval = p->getTermDatabase()->evaluateTerm( - inst, options::qcfTConstraint(), true); + Node inst_eval = + echeck->evaluateTerm(inst, options::qcfTConstraint(), true); if( Trace.isOn("qcf-instance-check") ){ Trace("qcf-instance-check") << "Possible propagating instance for " << d_q << " : " << std::endl; for( unsigned i=0; id_false; //} // modified - TermDb* tdb = p->getTermDatabase(); + EntailmentCheck* echeck = p->getTermRegistry().getEntailmentCheck(); QuantifiersState& qs = p->getState(); for (unsigned i = 0; i < 2; i++) { - if (tdb->isEntailed(d_n, i == 0)) + if (echeck->isEntailed(d_n, i == 0)) { d_ground_eval[0] = i==0 ? p->d_true : p->d_false; } @@ -1233,13 +1233,13 @@ bool MatchGen::reset_round(QuantConflictFind* p) } } }else if( d_type==typ_eq ){ - TermDb* tdb = p->getTermDatabase(); + EntailmentCheck* echeck = p->getTermRegistry().getEntailmentCheck(); QuantifiersState& qs = p->getState(); for (unsigned i = 0, size = d_n.getNumChildren(); i < size; i++) { if (!expr::hasBoundVar(d_n[i])) { - TNode t = tdb->getEntailedTerm(d_n[i]); + TNode t = echeck->getEntailedTerm(d_n[i]); if (qs.isInConflict()) { return false; @@ -1289,13 +1289,9 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) { TNode n = qi->getCurrentValue( d_n ); int vn = qi->getCurrentRepVar( qi->getVarNum( n ) ); if( vn==-1 ){ - //evaluate the value, see if it is compatible - //int e = p->evaluate( n ); - //if( ( e==1 && d_tgt ) || ( e==0 && !d_tgt ) ){ - // d_child_counter = 0; - //} - //modified - if( p->getTermDatabase()->isEntailed( n, d_tgt ) ){ + EntailmentCheck* echeck = p->getTermRegistry().getEntailmentCheck(); + if (echeck->isEntailed(n, d_tgt)) + { d_child_counter = 0; } }else{ @@ -2168,8 +2164,8 @@ void QuantConflictFind::checkQuantifiedFormula(Node q, Node inst = qinst->getInstantiation(q, terms); Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl; - Assert(!getTermDatabase()->isEntailed(inst, true)); - Assert(getTermDatabase()->isEntailed(inst, false) + Assert(!getTermRegistry().getEntailmentCheck()->isEntailed(inst, true)); + Assert(getTermRegistry().getEntailmentCheck()->isEntailed(inst, false) || d_effort > EFFORT_CONFLICT); } // Process the lemma: either add an instantiation or specific lemmas diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index b1537a390..573cab7bf 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -451,366 +451,6 @@ bool TermDb::inRelevantDomain( TNode f, unsigned i, TNode r ) { } } -Node TermDb::evaluateTerm2(TNode n, - std::map& visited, - std::vector& exp, - bool useEntailmentTests, - bool computeExp, - bool reqHasTerm) -{ - std::map< TNode, Node >::iterator itv = visited.find( n ); - if( itv != visited.end() ){ - return itv->second; - } - size_t prevSize = exp.size(); - Trace("term-db-eval") << "evaluate term : " << n << std::endl; - Node ret = n; - if( n.getKind()==FORALL || n.getKind()==BOUND_VARIABLE ){ - //do nothing - } - else if (d_qstate.hasTerm(n)) - { - Trace("term-db-eval") << "...exists in ee, return rep" << std::endl; - ret = d_qstate.getRepresentative(n); - if (computeExp) - { - if (n != ret) - { - exp.push_back(n.eqNode(ret)); - } - } - reqHasTerm = false; - } - else if (n.hasOperator()) - { - std::vector args; - bool ret_set = false; - Kind k = n.getKind(); - std::vector tempExp; - for (unsigned i = 0, nchild = n.getNumChildren(); i < nchild; i++) - { - TNode c = evaluateTerm2(n[i], - visited, - tempExp, - useEntailmentTests, - computeExp, - reqHasTerm); - if (c.isNull()) - { - ret = Node::null(); - ret_set = true; - break; - } - else if (c == d_true || c == d_false) - { - // short-circuiting - if ((k == AND && c == d_false) || (k == OR && c == d_true)) - { - ret = c; - ret_set = true; - reqHasTerm = false; - break; - } - else if (k == ITE && i == 0) - { - ret = evaluateTerm2(n[c == d_true ? 1 : 2], - visited, - tempExp, - useEntailmentTests, - computeExp, - reqHasTerm); - ret_set = true; - reqHasTerm = false; - break; - } - } - if (computeExp) - { - exp.insert(exp.end(), tempExp.begin(), tempExp.end()); - } - Trace("term-db-eval") << " child " << i << " : " << c << std::endl; - args.push_back(c); - } - if (ret_set) - { - // if we short circuited - if (computeExp) - { - exp.clear(); - exp.insert(exp.end(), tempExp.begin(), tempExp.end()); - } - } - else - { - // get the (indexed) operator of n, if it exists - TNode f = getMatchOperator(n); - // if it is an indexed term, return the congruent term - if (!f.isNull()) - { - // if f is congruent to a term indexed by this class - TNode nn = getCongruentTerm(f, args); - Trace("term-db-eval") << " got congruent term " << nn - << " from DB for " << n << std::endl; - if (!nn.isNull()) - { - if (computeExp) - { - Assert(nn.getNumChildren() == n.getNumChildren()); - for (unsigned i = 0, nchild = nn.getNumChildren(); i < nchild; i++) - { - if (nn[i] != n[i]) - { - exp.push_back(nn[i].eqNode(n[i])); - } - } - } - ret = d_qstate.getRepresentative(nn); - Trace("term-db-eval") << "return rep" << std::endl; - ret_set = true; - reqHasTerm = false; - Assert(!ret.isNull()); - if (computeExp) - { - if (n != ret) - { - exp.push_back(nn.eqNode(ret)); - } - } - } - } - if( !ret_set ){ - Trace("term-db-eval") << "return rewrite" << std::endl; - // a theory symbol or a new UF term - if (n.getMetaKind() == metakind::PARAMETERIZED) - { - args.insert(args.begin(), n.getOperator()); - } - ret = NodeManager::currentNM()->mkNode(n.getKind(), args); - ret = rewrite(ret); - if (ret.getKind() == EQUAL) - { - if (d_qstate.areDisequal(ret[0], ret[1])) - { - ret = d_false; - } - } - if (useEntailmentTests) - { - if (ret.getKind() == EQUAL || ret.getKind() == GEQ) - { - Valuation& val = d_qstate.getValuation(); - for (unsigned j = 0; j < 2; j++) - { - std::pair et = val.entailmentCheck( - options::TheoryOfMode::THEORY_OF_TYPE_BASED, - j == 0 ? ret : ret.negate()); - if (et.first) - { - ret = j == 0 ? d_true : d_false; - if (computeExp) - { - exp.push_back(et.second); - } - break; - } - } - } - } - } - } - } - // must have the term - if (reqHasTerm && !ret.isNull()) - { - Kind k = ret.getKind(); - if (k != OR && k != AND && k != EQUAL && k != ITE && k != NOT - && k != FORALL) - { - if (!d_qstate.hasTerm(ret)) - { - ret = Node::null(); - } - } - } - Trace("term-db-eval") << "evaluated term : " << n << ", got : " << ret - << ", reqHasTerm = " << reqHasTerm << std::endl; - // clear the explanation if failed - if (computeExp && ret.isNull()) - { - exp.resize(prevSize); - } - visited[n] = ret; - return ret; -} - -TNode TermDb::getEntailedTerm2(TNode n, - std::map& subs, - bool subsRep, - bool hasSubs) -{ - Trace("term-db-entail") << "get entailed term : " << n << std::endl; - if (d_qstate.hasTerm(n)) - { - Trace("term-db-entail") << "...exists in ee, return rep " << std::endl; - return n; - }else if( n.getKind()==BOUND_VARIABLE ){ - if( hasSubs ){ - std::map< TNode, TNode >::iterator it = subs.find( n ); - if( it!=subs.end() ){ - Trace("term-db-entail") << "...substitution is : " << it->second << std::endl; - if( subsRep ){ - Assert(d_qstate.hasTerm(it->second)); - Assert(d_qstate.getRepresentative(it->second) == it->second); - return it->second; - } - return getEntailedTerm2(it->second, subs, subsRep, hasSubs); - } - } - }else if( n.getKind()==ITE ){ - for( unsigned i=0; i<2; i++ ){ - if (isEntailed2(n[0], subs, subsRep, hasSubs, i == 0)) - { - return getEntailedTerm2(n[i == 0 ? 1 : 2], subs, subsRep, hasSubs); - } - } - }else{ - if( n.hasOperator() ){ - TNode f = getMatchOperator( n ); - if( !f.isNull() ){ - std::vector< TNode > args; - for( unsigned i=0; i visited; - std::vector exp; - return evaluateTerm2(n, visited, exp, useEntailmentTests, false, reqHasTerm); -} - -Node TermDb::evaluateTerm(TNode n, - std::vector& exp, - bool useEntailmentTests, - bool reqHasTerm) -{ - std::map visited; - return evaluateTerm2(n, visited, exp, useEntailmentTests, true, reqHasTerm); -} - -TNode TermDb::getEntailedTerm(TNode n, - std::map& subs, - bool subsRep) -{ - return getEntailedTerm2(n, subs, subsRep, true); -} - -TNode TermDb::getEntailedTerm(TNode n) -{ - std::map< TNode, TNode > subs; - return getEntailedTerm2(n, subs, false, false); -} - -bool TermDb::isEntailed2( - TNode n, std::map& subs, bool subsRep, bool hasSubs, bool pol) -{ - Trace("term-db-entail") << "Check entailed : " << n << ", pol = " << pol << std::endl; - Assert(n.getType().isBoolean()); - if( n.getKind()==EQUAL && !n[0].getType().isBoolean() ){ - TNode n1 = getEntailedTerm2(n[0], subs, subsRep, hasSubs); - if( !n1.isNull() ){ - TNode n2 = getEntailedTerm2(n[1], subs, subsRep, hasSubs); - if( !n2.isNull() ){ - if( n1==n2 ){ - return pol; - }else{ - Assert(d_qstate.hasTerm(n1)); - Assert(d_qstate.hasTerm(n2)); - if( pol ){ - return d_qstate.areEqual(n1, n2); - }else{ - return d_qstate.areDisequal(n1, n2); - } - } - } - } - }else if( n.getKind()==NOT ){ - return isEntailed2(n[0], subs, subsRep, hasSubs, !pol); - }else if( n.getKind()==OR || n.getKind()==AND ){ - bool simPol = ( pol && n.getKind()==OR ) || ( !pol && n.getKind()==AND ); - for( unsigned i=0; i subs; - return isEntailed2(n, subs, false, false, pol); -} - -bool TermDb::isEntailed(TNode n, - std::map& subs, - bool subsRep, - bool pol) -{ - Assert(d_consistent_ee); - return isEntailed2(n, subs, subsRep, true, pol); -} - bool TermDb::isTermActive( Node n ) { return d_inactive_map.find( n )==d_inactive_map.end(); //return !n.getAttribute(NoMatchAttribute()); diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index af0b87bd8..0e5c7bc01 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -176,78 +176,6 @@ class TermDb : public QuantifiersUtil { * equivalence class of r. */ bool inRelevantDomain(TNode f, unsigned i, TNode r); - /** evaluate term - * - * Returns a term n' such that n = n' is entailed based on the equality - * information ee. This function may generate new terms. In particular, - * we typically rewrite subterms of n of maximal size to terms that exist in - * the equality engine specified by ee. - * - * useEntailmentTests is whether to call the theory engine's entailmentTest - * on literals n for which this call fails to find a term n' that is - * equivalent to n, for increased precision. This is not frequently used. - * - * The vector exp stores the explanation for why n evaluates to that term, - * that is, if this call returns a non-null node n', then: - * exp => n = n' - * - * If reqHasTerm, then we require that the returned term is a Boolean - * combination of terms that exist in the equality engine used by this call. - * If no such term is constructable, this call returns null. The motivation - * for setting this to true is to "fail fast" if we require the return value - * of this function to only involve existing terms. This is used e.g. in - * the "propagating instances" portion of conflict-based instantiation - * (quant_conflict_find.h). - */ - Node evaluateTerm(TNode n, - std::vector& exp, - bool useEntailmentTests = false, - bool reqHasTerm = false); - /** same as above, without exp */ - Node evaluateTerm(TNode n, - bool useEntailmentTests = false, - bool reqHasTerm = false); - /** get entailed term - * - * If possible, returns a term n' such that: - * (1) n' exists in the current equality engine (as specified by the state), - * (2) n = n' is entailed in the current context. - * It returns null if no such term can be found. - * Wrt evaluateTerm, this version does not construct new terms, and - * thus is less aggressive. - */ - TNode getEntailedTerm(TNode n); - /** get entailed term - * - * If possible, returns a term n' such that: - * (1) n' exists in the current equality engine (as specified by the state), - * (2) n * subs = n' is entailed in the current context, where * denotes - * substitution application. - * It returns null if no such term can be found. - * subsRep is whether the substitution maps to terms that are representatives - * according to the quantifiers state. - * Wrt evaluateTerm, this version does not construct new terms, and - * thus is less aggressive. - */ - TNode getEntailedTerm(TNode n, std::map& subs, bool subsRep); - /** is entailed - * Checks whether the current context entails n with polarity pol, based on - * the equality information in the quantifiers state. Returns true if the - * entailment can be successfully shown. - */ - bool isEntailed(TNode n, bool pol); - /** is entailed - * - * Checks whether the current context entails ( n * subs ) with polarity pol, - * based on the equality information in the quantifiers state, - * where * denotes substitution application. - * subsRep is whether the substitution maps to terms that are representatives - * according to in the quantifiers state. - */ - bool isEntailed(TNode n, - std::map& subs, - bool subsRep, - bool pol); /** is the term n active in the current context? * * By default, all terms are active. A term is inactive if: @@ -355,24 +283,6 @@ class TermDb : public QuantifiersUtil { //----------------------------- end implementation-specific /** set has term */ void setHasTerm( Node n ); - /** helper for evaluate term */ - Node evaluateTerm2(TNode n, - std::map& visited, - std::vector& exp, - bool useEntailmentTests, - bool computeExp, - bool reqHasTerm); - /** helper for get entailed term */ - TNode getEntailedTerm2(TNode n, - std::map& subs, - bool subsRep, - bool hasSubs); - /** helper for is entailed */ - bool isEntailed2(TNode n, - std::map& subs, - bool subsRep, - bool hasSubs, - bool pol); /** compute uf eqc terms : * Ensure entries for f are in d_func_map_eqc_trie for all equivalence classes */ diff --git a/src/theory/quantifiers/term_registry.cpp b/src/theory/quantifiers/term_registry.cpp index ab999ad9b..d11fb0b8d 100644 --- a/src/theory/quantifiers/term_registry.cpp +++ b/src/theory/quantifiers/term_registry.cpp @@ -18,6 +18,7 @@ #include "options/base_options.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" +#include "theory/quantifiers/entailment_check.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/fmf/first_order_model_fmc.h" #include "theory/quantifiers/ho_term_database.h" @@ -39,6 +40,7 @@ TermRegistry::TermRegistry(Env& env, d_termPools(new TermPools(env, qs)), d_termDb(logicInfo().isHigherOrder() ? new HoTermDb(env, qs, qr) : new TermDb(env, qs, qr)), + d_echeck(new EntailmentCheck(env, qs, *d_termDb.get())), d_sygusTdb(nullptr), d_qmodel(nullptr) { @@ -132,6 +134,11 @@ TermDbSygus* TermRegistry::getTermDatabaseSygus() const return d_sygusTdb.get(); } +EntailmentCheck* TermRegistry::getEntailmentCheck() const +{ + return d_echeck.get(); +} + TermEnumeration* TermRegistry::getTermEnumeration() const { return d_termEnum.get(); diff --git a/src/theory/quantifiers/term_registry.h b/src/theory/quantifiers/term_registry.h index 175d450df..60a87a91f 100644 --- a/src/theory/quantifiers/term_registry.h +++ b/src/theory/quantifiers/term_registry.h @@ -23,6 +23,7 @@ #include "context/cdhashset.h" #include "smt/env_obj.h" +#include "theory/quantifiers/entailment_check.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_enumeration.h" @@ -83,6 +84,8 @@ class TermRegistry : protected EnvObj TermDb* getTermDatabase() const; /** get term database sygus */ TermDbSygus* getTermDatabaseSygus() const; + /** get entailment check utility */ + EntailmentCheck* getEntailmentCheck() const; /** get term enumeration utility */ TermEnumeration* getTermEnumeration() const; /** get the term pools utility */ @@ -103,6 +106,8 @@ class TermRegistry : protected EnvObj std::unique_ptr d_termPools; /** term database */ std::unique_ptr d_termDb; + /** entailment check */ + std::unique_ptr d_echeck; /** sygus term database */ std::unique_ptr d_sygusTdb; /** extended model object */ -- cgit v1.2.3 From 215519d099aee88bf53bddc71f071382484d29c0 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 14 Oct 2021 15:32:37 -0500 Subject: Improve parser for tuple select (#7364) --- src/parser/smt2/Smt2.g | 17 +++++------------ src/parser/smt2/smt2.cpp | 13 +++++++++---- src/parser/smt2/smt2.h | 2 +- 3 files changed, 15 insertions(+), 17 deletions(-) (limited to 'src') diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 478edb651..bff4f72ab 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1648,7 +1648,7 @@ identifier[cvc5::ParseOp& p] if (!f.getSort().isConstructor()) { PARSER_STATE->parseError( - "Bad syntax for test (_ is X), X must be a constructor."); + "Bad syntax for (_ is X), X must be a constructor."); } // get the datatype that f belongs to api::Sort sf = f.getSort().getConstructorCodomainSort(); @@ -1662,7 +1662,7 @@ identifier[cvc5::ParseOp& p] if (!f.getSort().isSelector()) { PARSER_STATE->parseError( - "Bad syntax for test (_ update X), X must be a selector."); + "Bad syntax for (_ update X), X must be a selector."); } std::string sname = f.toString(); // get the datatype that f belongs to @@ -1673,13 +1673,6 @@ identifier[cvc5::ParseOp& p] // get the updater term p.d_expr = ds.getUpdaterTerm(); } - | TUPLE_SEL_TOK m=INTEGER_LITERAL - { - // we adopt a special syntax (_ tupSel n) - p.d_kind = api::APPLY_SELECTOR; - // put m in expr so that the caller can deal with this case - p.d_expr = SOLVER->mkInteger(AntlrInput::tokenToUnsigned($m)); - } | TUPLE_PROJECT_TOK nonemptyNumeralList[numerals] { // we adopt a special syntax (_ tuple_project i_1 ... i_n) where @@ -1697,9 +1690,10 @@ identifier[cvc5::ParseOp& p] { std::string opName = AntlrInput::tokenText($sym); api::Kind k = PARSER_STATE->getIndexedOpKind(opName); - if (k == api::APPLY_UPDATER) + if (k == api::APPLY_SELECTOR || k == api::APPLY_UPDATER) { - // we adopt a special syntax (_ tuple_update n) for tuple updaters + // we adopt a special syntax (_ tuple_select n) and (_ tuple_update n) + // for tuple selectors and updaters if (numerals.size() != 1) { PARSER_STATE->parseError( @@ -2314,7 +2308,6 @@ FORALL_TOK : 'forall'; CHAR_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_STRINGS) }? 'char'; TUPLE_CONST_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'tuple'; -TUPLE_SEL_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'tuple_select'; TUPLE_PROJECT_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'tuple_project'; HO_ARROW_TOK : { PARSER_STATE->isHoEnabled() }? '->'; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index b186c2b2a..a69542b17 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -135,6 +135,11 @@ void Smt2::addDatatypesOperators() { Parser::addOperator(api::APPLY_UPDATER); addOperator(api::DT_SIZE, "dt.size"); + // Notice that tuple operators, we use the generic APPLY_SELECTOR and + // APPLY_UPDATER kinds. These are processed based on the context + // in which they are parsed, e.g. when parsing identifiers. + addIndexedOperator( + api::APPLY_SELECTOR, api::APPLY_SELECTOR, "tuple_select"); addIndexedOperator(api::APPLY_UPDATER, api::APPLY_UPDATER, "tuple_update"); } } @@ -288,7 +293,7 @@ void Smt2::addOperator(api::Kind kind, const std::string& name) Debug("parser") << "Smt2::addOperator( " << kind << ", " << name << " )" << std::endl; Parser::addOperator(kind); - operatorKindMap[name] = kind; + d_operatorKindMap[name] = kind; } void Smt2::addIndexedOperator(api::Kind tKind, @@ -302,11 +307,11 @@ void Smt2::addIndexedOperator(api::Kind tKind, api::Kind Smt2::getOperatorKind(const std::string& name) const { // precondition: isOperatorEnabled(name) - return operatorKindMap.find(name)->second; + return d_operatorKindMap.find(name)->second; } bool Smt2::isOperatorEnabled(const std::string& name) const { - return operatorKindMap.find(name) != operatorKindMap.end(); + return d_operatorKindMap.find(name) != d_operatorKindMap.end(); } bool Smt2::isTheoryEnabled(theory::TheoryId theory) const @@ -437,7 +442,7 @@ void Smt2::reset() { d_logicSet = false; d_seenSetLogic = false; d_logic = LogicInfo(); - operatorKindMap.clear(); + d_operatorKindMap.clear(); d_lastNamedTerm = std::pair(); } diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index fd68732fe..8d8f8febe 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -50,7 +50,7 @@ class Smt2 : public Parser bool d_seenSetLogic; LogicInfo d_logic; - std::unordered_map operatorKindMap; + std::unordered_map d_operatorKindMap; /** * Maps indexed symbols to the kind of the operator (e.g. "extract" to * BITVECTOR_EXTRACT). -- cgit v1.2.3 From b2329e04d3269587f968378db5fcdc0487dbbdb7 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 14 Oct 2021 15:16:58 -0700 Subject: Improve ManagedStreams (#7367) This PR addresses #7361, but also a more general issue about regular-output-channel being able to hold stderr and diagnostic-output-channel being able to hold stdout. It therefore changes how non-owned streams are stored: beforehand, an explicit stream would always be owned by the ManagedStream (through a std::shared_ptr) and a nullptr implicitly stood for stdout, stderr or stdin. Now we explicitly hold a pointer to a non-owned stream for these special values. Fixes #7361. --- src/options/managed_streams.cpp | 32 +++++++++++++---- src/options/managed_streams.h | 42 +++++++++++++++------- test/regress/CMakeLists.txt | 1 + test/regress/regress0/options/stream-printing.smt2 | 18 ++++++++++ 4 files changed, 74 insertions(+), 19 deletions(-) create mode 100644 test/regress/regress0/options/stream-printing.smt2 (limited to 'src') diff --git a/src/options/managed_streams.cpp b/src/options/managed_streams.cpp index 81bb242cf..90090df25 100644 --- a/src/options/managed_streams.cpp +++ b/src/options/managed_streams.cpp @@ -100,34 +100,54 @@ std::istream* openIStream(const std::string& filename) } } // namespace detail -std::ostream* ManagedErr::defaultValue() const { return &std::cerr; } +ManagedErr::ManagedErr() : ManagedStream(&std::cerr, "stderr") {} bool ManagedErr::specialCases(const std::string& value) { if (value == "stderr" || value == "--") { - d_stream.reset(); + d_nonowned = &std::cerr; + d_owned.reset(); + d_description = "stderr"; + return true; + } + else if (value == "stdout") + { + d_nonowned = &std::cout; + d_owned.reset(); + d_description = "stdout"; return true; } return false; } -std::istream* ManagedIn::defaultValue() const { return &std::cin; } +ManagedIn::ManagedIn() : ManagedStream(&std::cin, "stdin") {} bool ManagedIn::specialCases(const std::string& value) { if (value == "stdin" || value == "--") { - d_stream.reset(); + d_nonowned = &std::cin; + d_owned.reset(); + d_description = "stdin"; return true; } return false; } -std::ostream* ManagedOut::defaultValue() const { return &std::cout; } +ManagedOut::ManagedOut() : ManagedStream(&std::cout, "stdout") {} bool ManagedOut::specialCases(const std::string& value) { if (value == "stdout" || value == "--") { - d_stream.reset(); + d_nonowned = &std::cout; + d_owned.reset(); + d_description = "stdout"; + return true; + } + else if (value == "stderr") + { + d_nonowned = &std::cerr; + d_owned.reset(); + d_description = "stderr"; return true; } return false; diff --git a/src/options/managed_streams.h b/src/options/managed_streams.h index 56bb21c2e..cf1820de6 100644 --- a/src/options/managed_streams.h +++ b/src/options/managed_streams.h @@ -50,7 +50,8 @@ template class ManagedStream { public: - ManagedStream() {} + ManagedStream(Stream* nonowned, std::string description) + : d_nonowned(nonowned), d_description(std::move(description)) {} virtual ~ManagedStream() {} /** @@ -62,11 +63,15 @@ class ManagedStream if (specialCases(value)) return; if constexpr (std::is_same::value) { - d_stream.reset(detail::openOStream(value)); + d_nonowned = nullptr; + d_owned.reset(detail::openOStream(value)); + d_description = value; } else if constexpr (std::is_same::value) { - d_stream.reset(detail::openIStream(value)); + d_nonowned = nullptr; + d_owned.reset(detail::openIStream(value)); + d_description = value; } } @@ -75,12 +80,14 @@ class ManagedStream operator Stream&() const { return *getPtr(); } operator Stream*() const { return getPtr(); } + const std::string& description() const { return d_description; } + protected: - std::shared_ptr d_stream; + Stream* d_nonowned; + std::shared_ptr d_owned; + std::string d_description = ""; private: - /** Returns the value to be used if d_stream is not set. */ - virtual Stream* defaultValue() const = 0; /** * Check if there is a special case for this value. If so, the implementation * should set d_stream appropriately and return true to skip the default @@ -88,18 +95,18 @@ class ManagedStream */ virtual bool specialCases(const std::string& value) = 0; - /** Return the pointer, either from d_stream of from defaultValue(). */ + /** Return the pointer, either from d_nonowned or d_owned. */ Stream* getPtr() const { - if (d_stream) return d_stream.get(); - return defaultValue(); + if (d_nonowned != nullptr) return d_nonowned; + return d_owned.get(); } }; template std::ostream& operator<<(std::ostream& os, const ManagedStream& ms) { - return os << "ManagedStream"; + return os << ms.description(); } /** @@ -108,7 +115,10 @@ std::ostream& operator<<(std::ostream& os, const ManagedStream& ms) */ class ManagedErr : public ManagedStream { - std::ostream* defaultValue() const override final; + public: + ManagedErr(); + + private: bool specialCases(const std::string& value) override final; }; @@ -118,7 +128,10 @@ class ManagedErr : public ManagedStream */ class ManagedIn : public ManagedStream { - std::istream* defaultValue() const override final; + public: + ManagedIn(); + + private: bool specialCases(const std::string& value) override final; }; @@ -128,7 +141,10 @@ class ManagedIn : public ManagedStream */ class ManagedOut : public ManagedStream { - std::ostream* defaultValue() const override final; + public: + ManagedOut(); + + private: bool specialCases(const std::string& value) override final; }; diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index baced1e76..819bb94e4 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -769,6 +769,7 @@ set(regress_0_tests regress0/options/set-after-init.smt2 regress0/options/set-and-get-options.smt2 regress0/options/statistics.smt2 + regress0/options/stream-printing.smt2 regress0/parallel-let.smt2 regress0/parser/as.smt2 regress0/parser/bv_arity_smt2.6.smt2 diff --git a/test/regress/regress0/options/stream-printing.smt2 b/test/regress/regress0/options/stream-printing.smt2 new file mode 100644 index 000000000..21ea85aa1 --- /dev/null +++ b/test/regress/regress0/options/stream-printing.smt2 @@ -0,0 +1,18 @@ +; EXPECT: stdout +; EXPECT: stderr +; EXPECT: stdin +; EXPECT-ERROR: stderr +; EXPECT-ERROR: stdout +; EXPECT-ERROR: stdin + +(get-option :regular-output-channel) +(get-option :diagnostic-output-channel) +(get-option :in) + +(set-option :regular-output-channel stderr) +(set-option :diagnostic-output-channel stdout) +(set-option :in stdin) + +(get-option :regular-output-channel) +(get-option :diagnostic-output-channel) +(get-option :in) -- cgit v1.2.3 From 2e50a66e1cb58a86ff456948a6efff492487c21a Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 14 Oct 2021 16:38:21 -0700 Subject: Fix (get-info :authors) (#7373) This PR fixes calling (get-info :authors). It used to (try to) print the whole about() information, but failed to do so because the string needed to be turned into an s-expression. However, about() is not properly escaped. We now simply print the cvc5 authors. It also fixes isValidGetInfoFlag() which was missing filename. Fixes #7362. --- src/smt/solver_engine.cpp | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'src') diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index 911e0a960..e928dcade 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -417,10 +417,10 @@ void SolverEngine::setInfo(const std::string& key, const std::string& value) bool SolverEngine::isValidGetInfoFlag(const std::string& key) const { - if (key == "all-statistics" || key == "error-behavior" || key == "name" - || key == "version" || key == "authors" || key == "status" - || key == "reason-unknown" || key == "assertion-stack-levels" - || key == "all-options" || key == "time") + if (key == "all-statistics" || key == "error-behavior" || key == "filename" + || key == "name" || key == "version" || key == "authors" + || key == "status" || key == "time" || key == "reason-unknown" + || key == "assertion-stack-levels" || key == "all-options") { return true; } @@ -455,7 +455,7 @@ std::string SolverEngine::getInfo(const std::string& key) const } if (key == "authors") { - return toSExpr(Configuration::about()); + return toSExpr("the " + Configuration::getName() + " authors"); } if (key == "status") { -- cgit v1.2.3 From b4469530d2f6de599ddf7207a1914b88be49de5b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 15 Oct 2021 07:24:28 -0500 Subject: Fix issues related to proofs of lemmas with duplicate conclusions in strings (#7366) This makes string proof construction more robust by maintaining two separate proof inference constructors, one for facts and one for lemmas/conflicts. This avoids issues where 2 lemmas with the same conclusion (but possibly different explanations) are added in the same call to check. This fixes one of the two issues related to proofs for #6973. --- src/theory/strings/infer_proof_cons.cpp | 5 +++++ src/theory/strings/infer_proof_cons.h | 5 +++++ src/theory/strings/inference_manager.cpp | 15 ++++++++------- src/theory/strings/inference_manager.h | 9 ++++++++- src/theory/strings/regexp_solver.cpp | 5 ++++- test/regress/CMakeLists.txt | 1 + .../regress1/strings/issue6973-dup-lemma-conc.smt2 | 15 +++++++++++++++ 7 files changed, 46 insertions(+), 9 deletions(-) create mode 100644 test/regress/regress1/strings/issue6973-dup-lemma-conc.smt2 (limited to 'src') diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp index 34597c8be..5eba8663a 100644 --- a/src/theory/strings/infer_proof_cons.cpp +++ b/src/theory/strings/infer_proof_cons.cpp @@ -59,6 +59,11 @@ void InferProofCons::notifyFact(const InferInfo& ii) d_lazyFactMap.insert(ii.d_conc, iic); } +void InferProofCons::notifyLemma(const InferInfo& ii) +{ + d_lazyFactMap[ii.d_conc] = std::make_shared(ii); +} + bool InferProofCons::addProofTo(CDProof* pf, Node conc, InferenceId infer, diff --git a/src/theory/strings/infer_proof_cons.h b/src/theory/strings/infer_proof_cons.h index 110d231cf..02b266fd7 100644 --- a/src/theory/strings/infer_proof_cons.h +++ b/src/theory/strings/infer_proof_cons.h @@ -69,6 +69,11 @@ class InferProofCons : public ProofGenerator * only for facts that are explained. */ void notifyFact(const InferInfo& ii); + /** + * Same as above, but always overwrites. This is used for lemmas and + * conflicts, which do not necessarily have unique conclusions. + */ + void notifyLemma(const InferInfo& ii); /** * This returns the proof for fact. This is required for using this class as diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp index 0e971fc54..1f531a97c 100644 --- a/src/theory/strings/inference_manager.cpp +++ b/src/theory/strings/inference_manager.cpp @@ -42,7 +42,8 @@ InferenceManager::InferenceManager(Env& env, d_termReg(tr), d_extt(e), d_statistics(statistics), - d_ipc(pnm ? new InferProofCons(context(), pnm, d_statistics) : nullptr) + d_ipc(pnm ? new InferProofCons(context(), pnm, d_statistics) : nullptr), + d_ipcl(pnm ? new InferProofCons(context(), pnm, d_statistics) : nullptr) { NodeManager* nm = NodeManager::currentNM(); d_zero = nm->mkConst(Rational(0)); @@ -279,12 +280,12 @@ void InferenceManager::processConflict(const InferInfo& ii) { Assert(!d_state.isInConflict()); // setup the fact to reproduce the proof in the call below - if (d_ipc != nullptr) + if (d_ipcl != nullptr) { - d_ipc->notifyFact(ii); + d_ipcl->notifyLemma(ii); } // make the trust node - TrustNode tconf = mkConflictExp(ii.d_premises, d_ipc.get()); + TrustNode tconf = mkConflictExp(ii.d_premises, d_ipcl.get()); Assert(tconf.getKind() == TrustNodeKind::CONFLICT); Trace("strings-assert") << "(assert (not " << tconf.getNode() << ")) ; conflict " << ii.getId() << std::endl; @@ -335,11 +336,11 @@ TrustNode InferenceManager::processLemma(InferInfo& ii, LemmaProperty& p) } // ensure that the proof generator is ready to explain the final conclusion // of the lemma (ii.d_conc). - if (d_ipc != nullptr) + if (d_ipcl != nullptr) { - d_ipc->notifyFact(ii); + d_ipcl->notifyLemma(ii); } - TrustNode tlem = mkLemmaExp(ii.d_conc, exp, noExplain, d_ipc.get()); + TrustNode tlem = mkLemmaExp(ii.d_conc, exp, noExplain, d_ipcl.get()); Trace("strings-pending") << "Process pending lemma : " << tlem.getNode() << std::endl; diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h index 49f10d7cb..9f4cd1986 100644 --- a/src/theory/strings/inference_manager.h +++ b/src/theory/strings/inference_manager.h @@ -249,8 +249,15 @@ class InferenceManager : public InferenceManagerBuffered ExtTheory& d_extt; /** Reference to the statistics for the theory of strings/sequences. */ SequencesStatistics& d_statistics; - /** Conversion from inferences to proofs */ + /** Conversion from inferences to proofs for facts */ std::unique_ptr d_ipc; + /** + * Conversion from inferences to proofs for lemmas and conflicts. This is + * separate from the above proof generator to avoid rare cases where the + * conclusion of a lemma is a duplicate of the conclusion of another lemma, + * or is a fact in the current equality engine. + */ + std::unique_ptr d_ipcl; /** Common constants */ Node d_true; Node d_false; diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp index 614a5e6e0..898c0f1b7 100644 --- a/src/theory/strings/regexp_solver.cpp +++ b/src/theory/strings/regexp_solver.cpp @@ -546,7 +546,10 @@ bool RegExpSolver::checkPDerivative( { std::vector noExplain; noExplain.push_back(atom); - noExplain.push_back(x.eqNode(d_emptyString)); + if (x != d_emptyString) + { + noExplain.push_back(x.eqNode(d_emptyString)); + } std::vector iexp = nf_exp; iexp.insert(iexp.end(), noExplain.begin(), noExplain.end()); d_im.sendInference(iexp, noExplain, d_false, InferenceId::STRINGS_RE_DELTA_CONF); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 54fb91db4..587b2d9d6 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2204,6 +2204,7 @@ set(regress_1_tests regress1/strings/issue6653-rre-small.smt2 regress1/strings/issue6777-seq-nth-eval-cm.smt2 regress1/strings/issue6913.smt2 + regress1/strings/issue6973-dup-lemma-conc.smt2 regress1/strings/kaluza-fl.smt2 regress1/strings/loop002.smt2 regress1/strings/loop003.smt2 diff --git a/test/regress/regress1/strings/issue6973-dup-lemma-conc.smt2 b/test/regress/regress1/strings/issue6973-dup-lemma-conc.smt2 new file mode 100644 index 000000000..4c6fe5c62 --- /dev/null +++ b/test/regress/regress1/strings/issue6973-dup-lemma-conc.smt2 @@ -0,0 +1,15 @@ +(set-logic QF_SLIA) +(set-info :status unsat) +(declare-fun a () String) +(assert + (str.in_re "" + (re.++ (re.diff (re.comp re.all) (re.++ (str.to_re a) (re.comp re.all))) + (str.to_re + (ite + (str.in_re "" + (re.++ (str.to_re (ite (str.in_re "" (re.++ (str.to_re a) (re.comp re.all))) a "")) + (re.inter (str.to_re a) + (re.++ (str.to_re a) + (re.comp (re.union (re.++ (str.to_re a) (re.comp re.all)) re.all)))))) + a ""))))) +(check-sat) -- cgit v1.2.3 From 66a3314ce9a92112c6a89667f343085aca565ae5 Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Fri, 15 Oct 2021 13:45:03 -0700 Subject: Fix bad cast in the python API (#7359) --- src/api/python/cvc5.pxi | 8 ++++++-- test/python/unit/api/test_op.py | 3 +++ 2 files changed, 9 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 0f6b54dc6..e45f0206e 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -907,9 +907,10 @@ cdef class Solver: - ``Op mkOp(Kind kind, const string& arg)`` - ``Op mkOp(Kind kind, uint32_t arg)`` - ``Op mkOp(Kind kind, uint32_t arg0, uint32_t arg1)`` + - ``Op mkOp(Kind kind, [uint32_t arg0, ...])`` (used for the TupleProject kind) """ cdef Op op = Op(self) - cdef vector[int] v + cdef vector[uint32_t] v if len(args) == 0: op.cop = self.csolver.mkOp(k.k) @@ -922,7 +923,10 @@ cdef class Solver: op.cop = self.csolver.mkOp(k.k, args[0]) elif isinstance(args[0], list): for a in args[0]: - v.push_back(( a)) + if a < 0 or a >= 2 ** 31: + raise ValueError("Argument {} must fit in a uint32_t".format(a)) + + v.push_back(( a)) op.cop = self.csolver.mkOp(k.k, v) else: raise ValueError("Unsupported signature" diff --git a/test/python/unit/api/test_op.py b/test/python/unit/api/test_op.py index 07a57a5c6..5126a481d 100644 --- a/test/python/unit/api/test_op.py +++ b/test/python/unit/api/test_op.py @@ -86,6 +86,9 @@ def test_get_num_indices(solver): assert 2 == floatingpoint_to_fp_generic.getNumIndices() assert 2 == regexp_loop.getNumIndices() +def test_op_indices_list(solver): + with_list = solver.mkOp(kinds.TupleProject, [4, 25]) + assert 2 == with_list.getNumIndices() def test_get_indices_string(solver): x = Op(solver) -- cgit v1.2.3 From 538eea94a5861a6eb300c0cb2da381d217e6e73b Mon Sep 17 00:00:00 2001 From: yoni206 Date: Sat, 16 Oct 2021 02:09:02 +0300 Subject: Python api documentation: Op, Grammar, Result, Enums (#7095) This PR adds documentation to the python class Op, Grammar, Result, and for API enums. Additionally, documentation for isNull functions in the datatype classes is added for the python API, and a small change in the cpp API documentation is introduced. --- docs/api/cpp/cpp.rst | 1 + docs/api/cpp/unknownexplanation.rst | 6 ++ docs/api/python/grammar.rst | 6 ++ docs/api/python/op.rst | 6 ++ docs/api/python/python.rst | 5 ++ docs/api/python/result.rst | 6 ++ docs/api/python/roundingmode.rst | 6 ++ docs/api/python/unknownexplanation.rst | 6 ++ src/api/cpp/cvc5.h | 2 +- src/api/python/cvc5.pxi | 146 +++++++++++++++++++++++++++++---- 10 files changed, 173 insertions(+), 17 deletions(-) create mode 100644 docs/api/cpp/unknownexplanation.rst create mode 100644 docs/api/python/grammar.rst create mode 100644 docs/api/python/op.rst create mode 100644 docs/api/python/result.rst create mode 100644 docs/api/python/roundingmode.rst create mode 100644 docs/api/python/unknownexplanation.rst (limited to 'src') diff --git a/docs/api/cpp/cpp.rst b/docs/api/cpp/cpp.rst index c10ae7517..04f731203 100644 --- a/docs/api/cpp/cpp.rst +++ b/docs/api/cpp/cpp.rst @@ -30,5 +30,6 @@ C++ API Documentation sort statistics term + unknownexplanation diff --git a/docs/api/cpp/unknownexplanation.rst b/docs/api/cpp/unknownexplanation.rst new file mode 100644 index 000000000..9a64ec4aa --- /dev/null +++ b/docs/api/cpp/unknownexplanation.rst @@ -0,0 +1,6 @@ +UnknownExplanation +============ + +.. doxygenenum:: cvc5::api::Result::UnknownExplanation + :project: cvc5 + diff --git a/docs/api/python/grammar.rst b/docs/api/python/grammar.rst new file mode 100644 index 000000000..a2059fa93 --- /dev/null +++ b/docs/api/python/grammar.rst @@ -0,0 +1,6 @@ +Grammar +================ + +.. autoclass:: pycvc5.Grammar + :members: + :undoc-members: diff --git a/docs/api/python/op.rst b/docs/api/python/op.rst new file mode 100644 index 000000000..7769b33f0 --- /dev/null +++ b/docs/api/python/op.rst @@ -0,0 +1,6 @@ +Op +================ + +.. autoclass:: pycvc5.Op + :members: + :undoc-members: diff --git a/docs/api/python/python.rst b/docs/api/python/python.rst index d815f837a..a6aca2cf9 100644 --- a/docs/api/python/python.rst +++ b/docs/api/python/python.rst @@ -19,3 +19,8 @@ Python API Documentation datatypeconstructordecl datatypedecl datatypeselector + grammar + op + result + roundingmode + unknownexplanation diff --git a/docs/api/python/result.rst b/docs/api/python/result.rst new file mode 100644 index 000000000..9edb12b92 --- /dev/null +++ b/docs/api/python/result.rst @@ -0,0 +1,6 @@ +Result +================ + +.. autoclass:: pycvc5.Result + :members: + :undoc-members: diff --git a/docs/api/python/roundingmode.rst b/docs/api/python/roundingmode.rst new file mode 100644 index 000000000..0c226082e --- /dev/null +++ b/docs/api/python/roundingmode.rst @@ -0,0 +1,6 @@ +RoundingMode +================ + +.. autoclass:: pycvc5.RoundingMode + :members: + :undoc-members: diff --git a/docs/api/python/unknownexplanation.rst b/docs/api/python/unknownexplanation.rst new file mode 100644 index 000000000..54c37665b --- /dev/null +++ b/docs/api/python/unknownexplanation.rst @@ -0,0 +1,6 @@ +UnknownExplanation +================ + +.. autoclass:: pycvc5.UnknownExplanation + :members: + :undoc-members: diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 3db581db6..5e0f0d834 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -2464,7 +2464,7 @@ class CVC5_EXPORT Grammar /** * Allow \p ntSymbol to be any input variable to corresponding * synth-fun/synth-inv with the same sort as \p ntSymbol. - * @param ntSymbol the non-terminal allowed to be any input constant + * @param ntSymbol the non-terminal allowed to be any input variable */ void addAnyVariable(const Term& ntSymbol); diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index e45f0206e..2a35363ea 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -95,7 +95,10 @@ cdef c_hash[c_Term] ctermhash = c_hash[c_Term]() cdef class Datatype: - """Wrapper class for :cpp:class:`cvc5::api::Datatype`.""" + """ + A cvc5 datatype. + Wrapper class for :cpp:class:`cvc5::api::Datatype`. + """ cdef c_Datatype cd cdef Solver solver def __cinit__(self, Solver solver): @@ -114,7 +117,7 @@ cdef class Datatype: def getConstructor(self, str name): """ :param name: the name of the constructor. - :return: a constructor by name. + :return: a constructor by name. """ cdef DatatypeConstructor dc = DatatypeConstructor(self.solver) dc.cdc = self.cd.getConstructor(name.encode()) @@ -151,34 +154,35 @@ cdef class Datatype: return self.cd.getNumConstructors() def isParametric(self): - """:return: whether this datatype is parametric.""" + """:return: True if this datatype is parametric.""" return self.cd.isParametric() def isCodatatype(self): - """:return: whether this datatype corresponds to a co-datatype.""" + """:return: True if this datatype corresponds to a co-datatype.""" return self.cd.isCodatatype() def isTuple(self): - """:return: whether this datatype corresponds to a tuple.""" + """:return: True if this datatype corresponds to a tuple.""" return self.cd.isTuple() def isRecord(self): - """:return: whether this datatype corresponds to a record.""" + """:return: True if this datatype corresponds to a record.""" return self.cd.isRecord() def isFinite(self): - """:return: whether this datatype is finite.""" + """:return: True if this datatype is finite.""" return self.cd.isFinite() def isWellFounded(self): - """:return: whether this datatype is well-founded (see :cpp:func:`Datatype::isWellFounded() `).""" + """:return: True if this datatype is well-founded (see :cpp:func:`Datatype::isWellFounded() `).""" return self.cd.isWellFounded() def hasNestedRecursion(self): - """:return: whether this datatype has nested recursion (see :cpp:func:`Datatype::hasNestedRecursion() `).""" + """:return: True if this datatype has nested recursion (see :cpp:func:`Datatype::hasNestedRecursion() `).""" return self.cd.hasNestedRecursion() def isNull(self): + """:return: True if this Datatype is a null object.""" return self.cd.isNull() def __str__(self): @@ -195,7 +199,10 @@ cdef class Datatype: cdef class DatatypeConstructor: - """Wrapper class for :cpp:class:`cvc5::api::DatatypeConstructor`.""" + """ + A cvc5 datatype constructor. + Wrapper class for :cpp:class:`cvc5::api::DatatypeConstructor`. + """ cdef c_DatatypeConstructor cdc cdef Solver solver def __cinit__(self, Solver solver): @@ -270,6 +277,7 @@ cdef class DatatypeConstructor: return term def isNull(self): + """:return: True if this DatatypeConstructor is a null object.""" return self.cdc.isNull() def __str__(self): @@ -286,7 +294,10 @@ cdef class DatatypeConstructor: cdef class DatatypeConstructorDecl: - """Wrapper class for :cpp:class:`cvc5::api::DatatypeConstructorDecl`.""" + """ + A cvc5 datatype constructor declaration. + Wrapper class for :cpp:class:`cvc5::api::DatatypeConstructorDecl`. + """ cdef c_DatatypeConstructorDecl cddc cdef Solver solver @@ -311,6 +322,7 @@ cdef class DatatypeConstructorDecl: self.cddc.addSelectorSelf(name.encode()) def isNull(self): + """:return: True if this DatatypeConstructorDecl is a null object.""" return self.cddc.isNull() def __str__(self): @@ -321,7 +333,10 @@ cdef class DatatypeConstructorDecl: cdef class DatatypeDecl: - """Wrapper class for :cpp:class:`cvc5::api::DatatypeDecl`.""" + """ + A cvc5 datatype declaration. + Wrapper class for :cpp:class:`cvc5::api::DatatypeDecl`. + """ cdef c_DatatypeDecl cdd cdef Solver solver def __cinit__(self, Solver solver): @@ -354,6 +369,7 @@ cdef class DatatypeDecl: return self.cdd.getName().decode() def isNull(self): + """:return: True if this DatatypeDecl is a null object.""" return self.cdd.isNull() def __str__(self): @@ -364,7 +380,10 @@ cdef class DatatypeDecl: cdef class DatatypeSelector: - """Wrapper class for :cpp:class:`cvc5::api::DatatypeSelector`.""" + """ + A cvc5 datatype selector. + Wrapper class for :cpp:class:`cvc5::api::DatatypeSelector`. + """ cdef c_DatatypeSelector cds cdef Solver solver def __cinit__(self, Solver solver): @@ -402,6 +421,7 @@ cdef class DatatypeSelector: return sort def isNull(self): + """:return: True if this DatatypeSelector is a null object.""" return self.cds.isNull() def __str__(self): @@ -412,6 +432,13 @@ cdef class DatatypeSelector: cdef class Op: + """ + A cvc5 operator. + An operator is a term that represents certain operators, + instantiated with its required parameters, e.g., + a term of kind :cpp:enumerator:`BITVECTOR_EXTRACT`. + Wrapper class for :cpp:class:`cvc5::api::Op`. + """ cdef c_Op cop cdef Solver solver def __cinit__(self, Solver solver): @@ -434,18 +461,33 @@ cdef class Op: return cophash(self.cop) def getKind(self): + """ + :return: the kind of this operator. + """ return kind( self.cop.getKind()) def isIndexed(self): + """ + :return: True iff this operator is indexed. + """ return self.cop.isIndexed() def isNull(self): + """ + :return: True iff this operator is a null term. + """ return self.cop.isNull() def getNumIndices(self): + """ + :return: number of indices of this op. + """ return self.cop.getNumIndices() def getIndices(self): + """ + :return: the indices used to create this Op (see :cpp:func:`Op::getIndices() `). + """ indices = None try: indices = self.cop.getIndices[string]().decode() @@ -468,6 +510,10 @@ cdef class Op: return indices cdef class Grammar: + """ + A Sygus Grammar. + Wrapper class for :cpp:class:`cvc5::api::Grammar`. + """ cdef c_Grammar cgrammar cdef Solver solver def __cinit__(self, Solver solver): @@ -475,46 +521,100 @@ cdef class Grammar: self.cgrammar = c_Grammar() def addRule(self, Term ntSymbol, Term rule): + """ + Add ``rule`` to the set of rules corresponding to ``ntSymbol``. + + :param ntSymbol: the non-terminal to which the rule is added. + :param rule: the rule to add. + """ self.cgrammar.addRule(ntSymbol.cterm, rule.cterm) def addAnyConstant(self, Term ntSymbol): + """ + Allow ``ntSymbol`` to be an arbitrary constant. + + :param ntSymbol: the non-terminal allowed to be constant. + """ self.cgrammar.addAnyConstant(ntSymbol.cterm) def addAnyVariable(self, Term ntSymbol): + """ + Allow ``ntSymbol`` to be any input variable to corresponding synth-fun/synth-inv with the same sort as ``ntSymbol``. + + :param ntSymbol: the non-terminal allowed to be any input variable. + """ self.cgrammar.addAnyVariable(ntSymbol.cterm) def addRules(self, Term ntSymbol, rules): + """ + Add ``ntSymbol`` to the set of rules corresponding to ``ntSymbol``. + + :param ntSymbol: the non-terminal to which the rules are added. + :param rules: the rules to add. + """ cdef vector[c_Term] crules for r in rules: crules.push_back(( r).cterm) self.cgrammar.addRules(ntSymbol.cterm, crules) cdef class Result: + """ + Encapsulation of a three-valued solver result, with explanations. + Wrapper class for :cpp:class:`cvc5::api::Result`. + """ cdef c_Result cr def __cinit__(self): # gets populated by solver self.cr = c_Result() def isNull(self): + """ + :return: True if Result is empty, i.e., a nullary Result, + and not an actual result returned from a :cpp:func:`Solver::checkSat() ` (and friends) query. + """ return self.cr.isNull() def isSat(self): + """ + :return: True if query was a satisfiable :cpp:func:`Solver::checkSat() ` or :cpp:func:`Solver::checkSatAssuming() ` query. + """ return self.cr.isSat() def isUnsat(self): + """ + :return: True if query was an usatisfiable :cpp:func:`Solver::checkSat() ` or :cpp:func:`Solver::checkSatAssuming() ` query. + """ return self.cr.isUnsat() def isSatUnknown(self): + """ + :return: True if query was a :cpp:func:`Solver::checkSat() ` or :cpp:func:`Solver::checkSatAssuming() ` query and cvc5 was not able to determine (un)satisfiability. + """ return self.cr.isSatUnknown() def isEntailed(self): + """ + :return: True if corresponding query was an entailed :cpp:func:`Solver::checkEntailed() ` query. + """ return self.cr.isEntailed() def isNotEntailed(self): + """ + :return: True if corresponding query was a :cpp:func:`Solver::checkEntailed() ` query that is not entailed. + """ return self.cr.isNotEntailed() def isEntailmentUnknown(self): + """ + :return: True if query was a :cpp:func:`Solver::checkEntailed() ` query query and cvc5 was not able to determine if it is entailed. + """ return self.cr.isEntailmentUnknown() + + def getUnknownExplanation(self): + """ + :return: an explanation for an unknown query result. + """ + return UnknownExplanation( self.cr.getUnknownExplanation()) def __eq__(self, Result other): return self.cr == other.cr @@ -522,9 +622,6 @@ cdef class Result: def __ne__(self, Result other): return self.cr != other.cr - def getUnknownExplanation(self): - return UnknownExplanation( self.cr.getUnknownExplanation()) - def __str__(self): return self.cr.toString().decode() @@ -533,6 +630,20 @@ cdef class Result: cdef class RoundingMode: + """ + Rounding modes for floating-point numbers. + + For many floating-point operations, infinitely precise results may not be + representable with the number of available bits. Thus, the results are + rounded in a certain way to one of the representable floating-point numbers. + + These rounding modes directly follow the SMT-LIB theory for floating-point + arithmetic, which in turn is based on IEEE Standard 754 :cite:`IEEE754`. + The rounding modes are specified in Sections 4.3.1 and 4.3.2 of the IEEE + Standard 754. + + Wrapper class for :cpp:enum:`cvc5::api::RoundingMode`. + """ cdef c_RoundingMode crm cdef str name def __cinit__(self, int rm): @@ -557,6 +668,9 @@ cdef class RoundingMode: cdef class UnknownExplanation: + """ + Wrapper class for :cpp:enum:`cvc5::api::Result::UnknownExplanation`. + """ cdef c_UnknownExplanation cue cdef str name def __cinit__(self, int ue): -- cgit v1.2.3 From 3609bd8a3ef60a0ed61927567f5321eb28365858 Mon Sep 17 00:00:00 2001 From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> Date: Mon, 18 Oct 2021 17:50:04 -0500 Subject: Move check for experimental arrays features to `theory_arrays.cpp`. (#7391) Check for experimental array features was done at the parser module, which meant that users of the API could use them without calling Solver::setOption("arrays-exp"). This PR fixes that by moving the check to the internal theory module. --- src/parser/smt2/smt2.cpp | 5 ----- src/theory/arrays/theory_arrays.cpp | 17 +++++++++++++++-- test/regress/CMakeLists.txt | 1 + test/regress/regress0/eqrange0.smt2 | 6 ++++++ 4 files changed, 22 insertions(+), 7 deletions(-) create mode 100644 test/regress/regress0/eqrange0.smt2 (limited to 'src') diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index a69542b17..e1ce29b65 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1124,11 +1124,6 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector& args) Debug("parser") << "applyParseOp: return uminus " << ret << std::endl; return ret; } - if (kind == api::EQ_RANGE && d_solver->getOption("arrays-exp") != "true") - { - parseError( - "eqrange predicate requires option --arrays-exp to be enabled."); - } if (kind == api::SINGLETON && args.size() == 1) { api::Term ret = d_solver->mkTerm(api::SINGLETON, args[0]); diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 9e69c9f71..93eadde43 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -296,7 +296,19 @@ Node TheoryArrays::solveWrite(TNode term, bool solve1, bool solve2, bool ppCheck TrustNode TheoryArrays::ppRewrite(TNode term, std::vector& lems) { - // first, see if we need to expand definitions + // first, check for logic exceptions + Kind k = term.getKind(); + if (!options().arrays.arraysExp) + { + if (k == kind::EQ_RANGE) + { + std::stringstream ss; + ss << "Term of kind " << k + << " not supported in default mode, try --arrays-exp"; + throw LogicException(ss.str()); + } + } + // see if we need to expand definitions TrustNode texp = d_rewriter.expandDefinition(term); if (!texp.isNull()) { @@ -309,7 +321,8 @@ TrustNode TheoryArrays::ppRewrite(TNode term, std::vector& lems) d_ppEqualityEngine.addTerm(term); NodeManager* nm = NodeManager::currentNM(); Node ret; - switch (term.getKind()) { + switch (k) + { case kind::SELECT: { // select(store(a,i,v),j) = select(a,j) // IF i != j diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index da9c9f001..272867d0c 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -558,6 +558,7 @@ set(regress_0_tests regress0/distinct.smtv1.smt2 regress0/dump-unsat-core-full.smt2 regress0/echo.smt2 + regress0/eqrange0.smt2 regress0/eqrange1.smt2 regress0/eqrange2.smt2 regress0/eqrange3.smt2 diff --git a/test/regress/regress0/eqrange0.smt2 b/test/regress/regress0/eqrange0.smt2 new file mode 100644 index 000000000..01713d18f --- /dev/null +++ b/test/regress/regress0/eqrange0.smt2 @@ -0,0 +1,6 @@ +; EXPECT: (error "Term of kind EQ_RANGE not supported in default mode, try --arrays-exp") +; EXIT: 1 +(set-logic QF_AUFLIA) +(declare-const a (Array Int Int)) +(assert (eqrange a a 0 0)) +(check-sat) -- cgit v1.2.3 From 71842aa75ca106b14ded148a73ac856f3ecf5912 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Tue, 19 Oct 2021 12:33:25 -0700 Subject: Remove setDefaults methods (#7413) This PR removes some auto-generated utility methods to set an option if it has not been set by the user. It was once added as we thought it might be useful, but we do not actually use it. --- src/options/mkoptions.py | 34 ---------------------------------- src/options/module_template.cpp | 7 ------- src/options/module_template.h | 2 -- src/options/options_handler.cpp | 5 ++++- 4 files changed, 4 insertions(+), 44 deletions(-) (limited to 'src') diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py index a8f631de6..57f8b64e6 100644 --- a/src/options/mkoptions.py +++ b/src/options/mkoptions.py @@ -480,17 +480,6 @@ def generate_module_option_names(module): 'static constexpr const char* {name}__name = "{long_name}";', relevant) -def generate_module_setdefaults_decl(module): - res = [] - for option in module.options: - if option.name is None: - continue - funcname = option.name[0].capitalize() + option.name[1:] - res.append('void setDefault{}(Options& opts, {} value);'.format( - funcname, option.type)) - return '\n'.join(res) - - ################################################################################ # for options/.cpp @@ -581,27 +570,6 @@ def generate_module_mode_impl(module): return '\n'.join(res) -TPL_SETDEFAULT_IMPL = '''void setDefault{capname}(Options& opts, {type} value) -{{ - if (!opts.{module}.{name}WasSetByUser) opts.{module}.{name} = value; -}}''' - - -def generate_module_setdefaults_impl(module): - res = [] - for option in module.options: - if option.name is None: - continue - fmt = { - 'capname': option.name[0].capitalize() + option.name[1:], - 'type': option.type, - 'module': module.id, - 'name': option.name, - } - res.append(TPL_SETDEFAULT_IMPL.format(**fmt)) - return '\n'.join(res) - - ################################################################################ # for main/options.cpp @@ -875,11 +843,9 @@ def codegen_module(module, dst_dir, tpls): 'holder_decl': generate_module_holder_decl(module), 'wrapper_functions': generate_module_wrapper_functions(module), 'option_names': generate_module_option_names(module), - 'setdefaults_decl': generate_module_setdefaults_decl(module), # module source 'header': module.header, 'modes_impl': generate_module_mode_impl(module), - 'setdefaults_impl': generate_module_setdefaults_impl(module), } for tpl in tpls: filename = tpl['output'].replace('module', module.filename) diff --git a/src/options/module_template.cpp b/src/options/module_template.cpp index ee5260f34..d2ece3f13 100644 --- a/src/options/module_template.cpp +++ b/src/options/module_template.cpp @@ -28,11 +28,4 @@ namespace cvc5::options { ${modes_impl}$ // clang-format on -namespace ${id}$ -{ -// clang-format off -${setdefaults_impl}$ -// clang-format on -} - } // namespace cvc5::options diff --git a/src/options/module_template.h b/src/options/module_template.h index 61d689b72..d9b591f11 100644 --- a/src/options/module_template.h +++ b/src/options/module_template.h @@ -56,8 +56,6 @@ namespace ${id}$ { // clang-format off ${option_names}$ - -${setdefaults_decl}$ // clang-format on } diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 93b08a858..ec6c831e4 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -387,7 +387,10 @@ void OptionsHandler::checkBvSatSolver(const std::string& option, + " does not support lazy bit-blasting.\n" + "Try --bv-sat-solver=minisat"); } - options::bv::setDefaultBitvectorToBool(*d_options, true); + if (!d_options->bv.bitvectorToBoolWasSetByUser) + { + d_options->bv.bitvectorToBool = true; + } } } -- cgit v1.2.3 From 8fe459b1fb3843ebdbda86f24a414c46b986aa90 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 19 Oct 2021 15:35:13 -0500 Subject: Fix issue related to sanity checking integer models (#7363) We now insist that we sanity check integer models in linear logics. Previously, we could trigger an assertion failure in Minisat if a user asked for a model in a state where the linear solver had assigned a real value to an integer variable, as we would be sending a lemma during collectModelValues in a state where we had already terminated with "sat". This also changes an assertion to warning, to allow the regression to pass. Fixes #6774 (This PR fixes a followup issue after the original bad model reported there was fixed by sanity checks). As the assertion failure is downgraded to a warning, fixes #6988, fixes #7252. --- src/theory/arith/theory_arith.cpp | 23 ++++++++++++---------- test/regress/CMakeLists.txt | 3 +++ .../regress1/arith/issue6774-sanity-int-model.smt2 | 21 ++++++++++++++++++++ .../regress1/arith/issue7252-arith-sanity.smt2 | 14 +++++++++++++ .../regress1/cores/issue6988-arith-sanity.smt2 | 18 +++++++++++++++++ 5 files changed, 69 insertions(+), 10 deletions(-) create mode 100644 test/regress/regress1/arith/issue6774-sanity-int-model.smt2 create mode 100644 test/regress/regress1/arith/issue7252-arith-sanity.smt2 create mode 100644 test/regress/regress1/cores/issue6988-arith-sanity.smt2 (limited to 'src') diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 76a0c363d..cf2373b9f 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -193,9 +193,9 @@ void TheoryArith::postCheck(Effort level) if (Theory::fullEffort(level)) { d_arithModelCache.clear(); + std::set termSet; if (d_nonlinearExtension != nullptr) { - std::set termSet; updateModelCache(termSet); d_nonlinearExtension->checkFullEffort(d_arithModelCache, termSet); } @@ -204,6 +204,15 @@ void TheoryArith::postCheck(Effort level) // set incomplete d_im.setIncomplete(IncompleteId::ARITH_NL_DISABLED); } + // If we won't be doing a last call effort check (which implies that + // models will be computed), we must sanity check the integer model + // from the linear solver now. We also must update the model cache + // if we did not do so above. + if (d_nonlinearExtension == nullptr) + { + updateModelCache(termSet); + } + sanityCheckIntegerModel(); } } @@ -274,12 +283,6 @@ bool TheoryArith::collectModelValues(TheoryModel* m, updateModelCache(termSet); - if (sanityCheckIntegerModel()) - { - // We added a lemma - return false; - } - // We are now ready to assert the model. for (const std::pair& p : d_arithModelCache) { @@ -383,9 +386,9 @@ bool TheoryArith::sanityCheckIntegerModel() Trace("arith-check") << p.first << " -> " << p.second << std::endl; if (p.first.getType().isInteger() && !p.second.getType().isInteger()) { - Assert(false) << "TheoryArithPrivate generated a bad model value for " - "integer variable " - << p.first << " : " << p.second; + Warning() << "TheoryArithPrivate generated a bad model value for " + "integer variable " + << p.first << " : " << p.second; // must branch and bound TrustNode lem = d_bab.branchIntegerVariable(p.first, p.second.getConst()); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index b1d776b21..84f0ef408 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1505,6 +1505,8 @@ set(regress_1_tests regress1/arith/issue3952-rew-eq.smt2 regress1/arith/issue4985-model-success.smt2 regress1/arith/issue4985b-model-success.smt2 + regress1/arith/issue6774-sanity-int-model.smt2 + regress1/arith/issue7252-arith-sanity.smt2 regress1/arith/issue789.smt2 regress1/arith/miplib3.cvc.smt2 regress1/arith/mod.02.smt2 @@ -1576,6 +1578,7 @@ set(regress_1_tests regress1/constarr3.cvc.smt2 regress1/constarr3.smt2 regress1/cores/issue5604.smt2 + regress1/cores/issue6988-arith-sanity.smt2 regress1/datatypes/acyclicity-sr-ground096.smt2 regress1/datatypes/cee-prs-small-dd2.smt2 regress1/datatypes/dt-color-2.6.smt2 diff --git a/test/regress/regress1/arith/issue6774-sanity-int-model.smt2 b/test/regress/regress1/arith/issue6774-sanity-int-model.smt2 new file mode 100644 index 000000000..732b709f9 --- /dev/null +++ b/test/regress/regress1/arith/issue6774-sanity-int-model.smt2 @@ -0,0 +1,21 @@ +; COMMAND-LINE: -i -q +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +(set-logic ALIRA) +(declare-const x Real) +(declare-fun i () Int) +(declare-fun i1 () Int) +(push) +(assert (< 1 (- i))) +(check-sat) +(pop) +(push) +(assert (or (>= i1 (* 5 (- i))))) +(check-sat) +(pop) +(assert (or (> i1 1) (= x (to_real i)))) +(check-sat) +(assert (not (is_int x))) +(check-sat) diff --git a/test/regress/regress1/arith/issue7252-arith-sanity.smt2 b/test/regress/regress1/arith/issue7252-arith-sanity.smt2 new file mode 100644 index 000000000..dd7a1fa2e --- /dev/null +++ b/test/regress/regress1/arith/issue7252-arith-sanity.smt2 @@ -0,0 +1,14 @@ +; COMMAND-LINE: -q +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) +(declare-fun a () Int) +(declare-fun b () Int) +(declare-fun c () Int) +(declare-fun d () Int) +(declare-fun e () Int) +(declare-fun f () Int) +(declare-fun g () Int) +(assert (> 0 (* a (mod 0 b)))) +(assert (or (and (> (* b d) (* 2 (+ g c))) (= g (- c)) (> (+ e c) 0)) (> f 0))) +(check-sat) diff --git a/test/regress/regress1/cores/issue6988-arith-sanity.smt2 b/test/regress/regress1/cores/issue6988-arith-sanity.smt2 new file mode 100644 index 000000000..622d64375 --- /dev/null +++ b/test/regress/regress1/cores/issue6988-arith-sanity.smt2 @@ -0,0 +1,18 @@ +; COMMAND-LINE: -i -q +; EXPECT: sat +; EXPECT: sat +(set-logic ANIA) +(declare-const x Bool) +(set-option :produce-unsat-cores true) +(declare-fun i () Int) +(declare-fun i5 () Int) +(declare-fun i8 () Int) +(assert (or x (< i5 0))) +(push) +(assert (and (= i8 1) (= i5 (+ 1 i)) (= i8 (+ 1 i)))) +(push) +(check-sat) +(pop) +(pop) +(assert (= i8 (* i8 3 (+ i8 1)))) +(check-sat) -- cgit v1.2.3 From bda77d20d51b0ebdd8dec4bd50c6ce5faef7f218 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 19 Oct 2021 18:01:11 -0500 Subject: Support sequences of fixed finite cardinality (#7371) The only open case is dynamic cardinality types (e.g. uninterpreted sorts when FMF is enabled). --- src/theory/incomplete_id.cpp | 2 ++ src/theory/incomplete_id.h | 5 +++ src/theory/strings/base_solver.cpp | 38 ++++++++++++++++++++-- test/regress/CMakeLists.txt | 1 + test/regress/regress1/strings/seq-cardinality.smt2 | 11 +++++++ 5 files changed, 55 insertions(+), 2 deletions(-) create mode 100644 test/regress/regress1/strings/seq-cardinality.smt2 (limited to 'src') diff --git a/src/theory/incomplete_id.cpp b/src/theory/incomplete_id.cpp index a2a3baa0f..c763fb9a0 100644 --- a/src/theory/incomplete_id.cpp +++ b/src/theory/incomplete_id.cpp @@ -40,6 +40,8 @@ const char* toString(IncompleteId i) case IncompleteId::STRINGS_LOOP_SKIP: return "STRINGS_LOOP_SKIP"; case IncompleteId::STRINGS_REGEXP_NO_SIMPLIFY: return "STRINGS_REGEXP_NO_SIMPLIFY"; + case IncompleteId::SEQ_FINITE_DYNAMIC_CARDINALITY: + return "SEQ_FINITE_DYNAMIC_CARDINALITY"; case IncompleteId::UF_HO_EXT_DISABLED: return "UF_HO_EXT_DISABLED"; case IncompleteId::UF_CARD_DISABLED: return "UF_CARD_DISABLED"; case IncompleteId::UF_CARD_MODE: return "UF_CARD_MODE"; diff --git a/src/theory/incomplete_id.h b/src/theory/incomplete_id.h index 951c2a94f..aaa458d8e 100644 --- a/src/theory/incomplete_id.h +++ b/src/theory/incomplete_id.h @@ -52,6 +52,11 @@ enum class IncompleteId STRINGS_LOOP_SKIP, // we could not simplify a regular expression membership STRINGS_REGEXP_NO_SIMPLIFY, + // incomplete due to sequence of a dynamic finite type (e.g. a type that + // we know is finite, but its exact cardinality is not fixed. For example, + // when finite model finding is enabled, uninterpreted sorts have a + // cardinality that depends on their interpretation in the current model). + SEQ_FINITE_DYNAMIC_CARDINALITY, // HO extensionality axiom was disabled UF_HO_EXT_DISABLED, // UF+cardinality solver was disabled diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp index b675d2444..9396e3e87 100644 --- a/src/theory/strings/base_solver.cpp +++ b/src/theory/strings/base_solver.cpp @@ -17,6 +17,7 @@ #include "theory/strings/base_solver.h" #include "expr/sequence.h" +#include "options/quantifiers_options.h" #include "options/strings_options.h" #include "theory/rewriter.h" #include "theory/strings/theory_strings_utils.h" @@ -539,8 +540,41 @@ void BaseSolver::checkCardinalityType(TypeNode tn, // infinite cardinality, we are fine return; } - // TODO (cvc4-projects #23): how to handle sequence for finite types? - return; + // we check the cardinality class of the type, assuming that FMF is + // disabled. + if (isCardinalityClassFinite(etn.getCardinalityClass(), false)) + { + Cardinality c = etn.getCardinality(); + bool smallCardinality = false; + if (!c.isLargeFinite()) + { + Integer ci = c.getFiniteCardinality(); + if (ci.fitsUnsignedInt()) + { + smallCardinality = true; + typeCardSize = ci.toUnsignedInt(); + } + } + if (!smallCardinality) + { + // if it is large finite, then there is no way we could have + // constructed that many terms in memory, hence there is nothing + // to do. + return; + } + } + else + { + Assert(options().quantifiers.finiteModelFind); + // we are in a case where the cardinality of the type is infinite + // if not FMF, and finite given the Env's option value for FMF. In this + // case, FMF must be true, and the cardinality is finite and dynamic + // (i.e. it depends on the model's finite interpretation for uninterpreted + // sorts). We do not know how to handle this case, we set incomplete. + // TODO (cvc4-projects #23): how to handle sequence for finite types? + d_im.setIncomplete(IncompleteId::SEQ_FINITE_DYNAMIC_CARDINALITY); + return; + } } // for each collection for (unsigned i = 0, csize = cols.size(); i < csize; ++i) diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 84f0ef408..a0f6f7999 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2268,6 +2268,7 @@ set(regress_1_tests regress1/strings/rev-ex5.smt2 regress1/strings/rew-020618.smt2 regress1/strings/rew-check1.smt2 + regress1/strings/seq-cardinality.smt2 regress1/strings/seq-quant-infinite-branch.smt2 regress1/strings/simple-re-consume.smt2 regress1/strings/stoi-400million.smt2 diff --git a/test/regress/regress1/strings/seq-cardinality.smt2 b/test/regress/regress1/strings/seq-cardinality.smt2 new file mode 100644 index 000000000..93a4985d4 --- /dev/null +++ b/test/regress/regress1/strings/seq-cardinality.smt2 @@ -0,0 +1,11 @@ +(set-logic ALL) +(set-info :status unsat) +(declare-fun x () (Seq (_ BitVec 1))) +(declare-fun y () (Seq (_ BitVec 1))) +(declare-fun z () (Seq (_ BitVec 1))) + +(assert (= (seq.len x) 1)) +(assert (= (seq.len y) 1)) +(assert (= (seq.len z) 1)) +(assert (distinct x y z)) +(check-sat) -- cgit v1.2.3 From a96ed1538245b2ce2cd8a8084e0288d07071ca23 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 19 Oct 2021 18:53:56 -0500 Subject: Fix expected conclusion for EQ_RESOLVE when expanding MACRO_SR_PRED_TRANSFORM (#7412) Fixes a proof checking failure during post-processing. Fixes a rare case where the RHS of equality resolve step requires a symmetry step. --- src/smt/proof_post_processor.cpp | 2 +- test/regress/CMakeLists.txt | 1 + test/regress/regress1/proofs/qgu-fuzz-1-strings-pp.smt2 | 5 +++++ 3 files changed, 7 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress1/proofs/qgu-fuzz-1-strings-pp.smt2 (limited to 'src') diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index adc15ca2c..a547c4362 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -654,7 +654,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, // apply transitivity if necessary Node eq = addProofForTrans(tchildren, cdp); - cdp->addStep(args[0], PfRule::EQ_RESOLVE, {children[0], eq}, {}); + cdp->addStep(eq[1], PfRule::EQ_RESOLVE, {children[0], eq}, {}); return args[0]; } else if (id == PfRule::MACRO_RESOLUTION diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index a0f6f7999..81b2bd0c9 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1763,6 +1763,7 @@ set(regress_1_tests regress1/proofs/issue6625-unsat-core-proofs.smt2 regress1/proofs/macro-res-exp-crowding-lit-inside-unit.smt2 regress1/proofs/macro-res-exp-singleton-after-elimCrowd.smt2 + regress1/proofs/qgu-fuzz-1-strings-pp.smt2 regress1/proofs/quant-alpha-eq.smt2 regress1/proofs/sat-trivial-cycle.smt2 regress1/proofs/unsat-cores-proofs.smt2 diff --git a/test/regress/regress1/proofs/qgu-fuzz-1-strings-pp.smt2 b/test/regress/regress1/proofs/qgu-fuzz-1-strings-pp.smt2 new file mode 100644 index 000000000..c0c1f16f7 --- /dev/null +++ b/test/regress/regress1/proofs/qgu-fuzz-1-strings-pp.smt2 @@ -0,0 +1,5 @@ +(set-logic ALL) +(set-info :status unsat) +(declare-fun x () String) +(assert (let ((_let_1 (str.to_re "B"))) (and (str.in_re x (re.++ re.allchar (str.to_re (str.++ "B" "A")))) (str.in_re x (re.* (re.union re.allchar (str.to_re "A")))) (str.in_re x (re.* (re.union re.allchar _let_1))) (str.in_re x (re.* (re.++ re.allchar _let_1)))))) +(check-sat) -- cgit v1.2.3 From fc9c1005a398c537bdb491d1b161f3e316b68b5e Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 19 Oct 2021 19:24:32 -0500 Subject: Add basic regular expression type enumerator (#7416) The lack of a type enumerator for regular expressions makes certain things impossible e.g. sygus-based sampling for RE queries. It is trivial to support a basic RE enumerator that takes singleton languages of strings. This commit adds this utility as the type enumerator for RE. --- src/CMakeLists.txt | 2 ++ src/theory/strings/kinds | 4 +++ src/theory/strings/regexp_enumerator.cpp | 49 ++++++++++++++++++++++++++ src/theory/strings/regexp_enumerator.h | 59 ++++++++++++++++++++++++++++++++ 4 files changed, 114 insertions(+) create mode 100644 src/theory/strings/regexp_enumerator.cpp create mode 100644 src/theory/strings/regexp_enumerator.h (limited to 'src') diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 374c57726..cde739454 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -1081,6 +1081,8 @@ libcvc5_add_sources( theory/strings/normal_form.h theory/strings/proof_checker.cpp theory/strings/proof_checker.h + theory/strings/regexp_enumerator.cpp + theory/strings/regexp_enumerator.h theory/strings/regexp_elim.cpp theory/strings/regexp_elim.h theory/strings/regexp_entail.cpp diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index aa95ef2f8..9faa935e1 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -56,6 +56,10 @@ enumerator STRING_TYPE \ "::cvc5::theory::strings::StringEnumerator" \ "theory/strings/type_enumerator.h" +enumerator REGEXP_TYPE \ + "::cvc5::theory::strings::RegExpEnumerator" \ + "theory/strings/regexp_enumerator.h" + constant CONST_STRING \ class \ String \ diff --git a/src/theory/strings/regexp_enumerator.cpp b/src/theory/strings/regexp_enumerator.cpp new file mode 100644 index 000000000..261d0008e --- /dev/null +++ b/src/theory/strings/regexp_enumerator.cpp @@ -0,0 +1,49 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Implementation of enumerator for regular expressions. + */ + +#include "theory/strings/regexp_enumerator.h" + +namespace cvc5 { +namespace theory { +namespace strings { + +RegExpEnumerator::RegExpEnumerator(TypeNode type, TypeEnumeratorProperties* tep) + : TypeEnumeratorBase(type), d_senum(type, tep) +{ +} + +RegExpEnumerator::RegExpEnumerator(const RegExpEnumerator& enumerator) + : TypeEnumeratorBase(enumerator.getType()), + d_senum(enumerator.d_senum) +{ +} + +Node RegExpEnumerator::operator*() +{ + NodeManager* nm = NodeManager::currentNM(); + return nm->mkNode(kind::STRING_TO_REGEXP, *d_senum); +} + +RegExpEnumerator& RegExpEnumerator::operator++() +{ + ++d_senum; + return *this; +} + +bool RegExpEnumerator::isFinished() { return d_senum.isFinished(); } + +} // namespace strings +} // namespace theory +} // namespace cvc5 diff --git a/src/theory/strings/regexp_enumerator.h b/src/theory/strings/regexp_enumerator.h new file mode 100644 index 000000000..289c8b046 --- /dev/null +++ b/src/theory/strings/regexp_enumerator.h @@ -0,0 +1,59 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Enumerators for regular expressions. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__THEORY__STRINGS__REGEXP_ENUMERATOR_H +#define CVC5__THEORY__STRINGS__REGEXP_ENUMERATOR_H + +#include + +#include "expr/node.h" +#include "expr/type_node.h" +#include "theory/strings/type_enumerator.h" + +namespace cvc5 { +namespace theory { +namespace strings { + +/** + * Simple regular expression enumerator, generates only singleton language + * regular expressions from a string enumeration, in other words: + * (str.to_re s1) ... (str.to_re sn) .... + * where s1 ... sn ... is the enumeration for strings. + */ +class RegExpEnumerator : public TypeEnumeratorBase +{ + public: + RegExpEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr); + RegExpEnumerator(const RegExpEnumerator& enumerator); + ~RegExpEnumerator() {} + /** get the current term */ + Node operator*() override; + /** increment */ + RegExpEnumerator& operator++() override; + /** is this enumerator finished? */ + bool isFinished() override; + + private: + /** underlying string enumerator */ + StringEnumerator d_senum; +}; + +} // namespace strings +} // namespace theory +} // namespace cvc5 + +#endif /* CVC5__THEORY__STRINGS__TYPE_ENUMERATOR_H */ -- cgit v1.2.3 From f047038b1bec31a1ebb89e9d35e3aebb3301eddc Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 19 Oct 2021 19:35:14 -0500 Subject: Make proofs of rewrites robust to use in internal subsolvers (#7411) We are currently using an attribute to mark "rewritten with proofs". This is incorrect as attributes are global, but proofs of rewrites are local to the solver instance. This enables applications of proofs within internal subsolvers, and is required for a new internal fuzzing technique. --- src/theory/rewriter.cpp | 22 ++++++++++------------ src/theory/rewriter.h | 11 +++++++++++ 2 files changed, 21 insertions(+), 12 deletions(-) (limited to 'src') diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 6cb3bf3ff..361d90dcd 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -32,13 +32,6 @@ using namespace std; namespace cvc5 { namespace theory { -/** Attribute true for nodes that have been rewritten with proofs enabled */ -struct RewriteWithProofsAttributeId -{ -}; -typedef expr::Attribute - RewriteWithProofsAttribute; - // Note that this function is a simplified version of Theory::theoryOf for // (type-based) theoryOfMode. We expand and simplify it here for the sake of // efficiency. @@ -173,7 +166,6 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node, TConvProofGenerator* tcpg) { - RewriteWithProofsAttribute rpfa; #ifdef CVC5_ASSERTIONS bool isEquality = node.getKind() == kind::EQUAL && (!node[0].getType().isBoolean()); @@ -187,7 +179,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, // Check if it's been cached already Node cached = getPostRewriteCache(theoryId, node); - if (!cached.isNull() && (tcpg == nullptr || node.getAttribute(rpfa))) + if (!cached.isNull() && (tcpg == nullptr || hasRewrittenWithProofs(node))) { return cached; } @@ -217,7 +209,8 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, cached = getPreRewriteCache(rewriteStackTop.getTheoryId(), rewriteStackTop.d_node); if (cached.isNull() - || (tcpg != nullptr && !rewriteStackTop.d_node.getAttribute(rpfa))) + || (tcpg != nullptr + && !hasRewrittenWithProofs(rewriteStackTop.d_node))) { // Rewrite until fix-point is reached for(;;) { @@ -256,7 +249,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, rewriteStackTop.d_node); // If not, go through the children if (cached.isNull() - || (tcpg != nullptr && !rewriteStackTop.d_node.getAttribute(rpfa))) + || (tcpg != nullptr && !hasRewrittenWithProofs(rewriteStackTop.d_node))) { // The child we need to rewrite unsigned child = rewriteStackTop.d_nextChild++; @@ -343,7 +336,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, if (tcpg != nullptr) { // if proofs are enabled, mark that we've rewritten with proofs - rewriteStackTop.d_original.setAttribute(rpfa, true); + d_tpgNodes.insert(rewriteStackTop.d_original); if (!cached.isNull()) { // We may have gotten a different node, due to non-determinism in @@ -474,5 +467,10 @@ void Rewriter::clearCaches() clearCachesInternal(); } +bool Rewriter::hasRewrittenWithProofs(TNode n) const +{ + return d_tpgNodes.find(n) != d_tpgNodes.end(); +} + } // namespace theory } // namespace cvc5 diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h index f96062b61..d90af4a31 100644 --- a/src/theory/rewriter.h +++ b/src/theory/rewriter.h @@ -159,6 +159,11 @@ class Rewriter { void clearCachesInternal(); + /** + * Has n been rewritten with proofs? This checks if n is in d_tpgNodes. + */ + bool hasRewrittenWithProofs(TNode n) const; + /** The resource manager, for tracking resource usage */ ResourceManager* d_resourceManager; @@ -167,6 +172,12 @@ class Rewriter { /** The proof generator */ std::unique_ptr d_tpg; + /** + * Nodes rewritten with proofs. Since d_tpg contains a reference to all + * nodes that have been rewritten with proofs, we can keep only a TNode + * here. + */ + std::unordered_set d_tpgNodes; #ifdef CVC5_ASSERTIONS std::unique_ptr> d_rewriteStack = nullptr; #endif /* CVC5_ASSERTIONS */ -- cgit v1.2.3 From 3ae2c455dbb6ac95834fd23082688b11784dfcae Mon Sep 17 00:00:00 2001 From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> Date: Tue, 19 Oct 2021 20:11:53 -0500 Subject: Avoid escaping `double-quotes` twice. (#7409) With -o raw-benchmark, The command: (echo """") was printed as (echo """""""") because we run the quote-escaping procedure twice on it. This PR fixes the issue by ensuring that we only run it once. --- src/parser/smt2/Smt2.g | 2 +- src/printer/smt2/smt2_printer.cpp | 21 ++++----------------- src/smt/command.cpp | 17 +++++------------ src/util/smt2_quote_string.cpp | 12 ++++++++++++ src/util/smt2_quote_string.h | 5 +++++ 5 files changed, 27 insertions(+), 30 deletions(-) (limited to 'src') diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index bff4f72ab..a75aa36da 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -793,7 +793,7 @@ smt25Command[std::unique_ptr* cmd] /* echo */ | ECHO_TOK - ( simpleSymbolicExpr[s] + ( str[s, true] { cmd->reset(new EchoCommand(s)); } | { cmd->reset(new EchoCommand()); } ) diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 32b195be2..1da2a3c7b 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1723,15 +1723,7 @@ void Smt2Printer::toStreamCmdEmpty(std::ostream& out, void Smt2Printer::toStreamCmdEcho(std::ostream& out, const std::string& output) const { - std::string s = output; - // escape all double-quotes - size_t pos = 0; - while ((pos = s.find('"', pos)) != string::npos) - { - s.replace(pos, 1, "\"\""); - pos += 2; - } - out << "(echo \"" << s << "\")" << std::endl; + out << "(echo " << cvc5::quoteString(output) << ')' << std::endl; } /* @@ -1930,14 +1922,9 @@ static void toStream(std::ostream& out, const CommandUnsupported* s, Variant v) #endif /* CVC5_COMPETITION_MODE */ } -static void errorToStream(std::ostream& out, std::string message, Variant v) { - // escape all double-quotes - size_t pos = 0; - while((pos = message.find('"', pos)) != string::npos) { - message.replace(pos, 1, "\"\""); - pos += 2; - } - out << "(error \"" << message << "\")" << endl; +static void errorToStream(std::ostream& out, std::string message, Variant v) +{ + out << "(error " << cvc5::quoteString(message) << ')' << endl; } static void toStream(std::ostream& out, const CommandFailure* s, Variant v) { diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 311d6713a..e8ee6d59c 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -38,6 +38,7 @@ #include "proof/unsat_core.h" #include "smt/dump.h" #include "smt/model.h" +#include "util/smt2_quote_string.h" #include "util/unsafe_interrupt_exception.h" #include "util/utility.h" @@ -302,19 +303,10 @@ void EmptyCommand::toStream(std::ostream& out, /* class EchoCommand */ /* -------------------------------------------------------------------------- */ -EchoCommand::EchoCommand(std::string output) -{ - // escape all double-quotes - size_t pos = 0; - while ((pos = output.find('"', pos)) != string::npos) - { - output.replace(pos, 1, "\"\""); - pos += 2; - } - d_output = '"' + output + '"'; -} +EchoCommand::EchoCommand(std::string output) : d_output(output) {} std::string EchoCommand::getOutput() const { return d_output; } + void EchoCommand::invoke(api::Solver* solver, SymbolManager* sm) { /* we don't have an output stream here, nothing to do */ @@ -325,7 +317,7 @@ void EchoCommand::invoke(api::Solver* solver, SymbolManager* sm, std::ostream& out) { - out << d_output << std::endl; + out << cvc5::quoteString(d_output) << std::endl; Trace("dtview::command") << "* ~COMMAND: echo |" << d_output << "|~" << std::endl; d_commandStatus = CommandSuccess::instance(); @@ -335,6 +327,7 @@ void EchoCommand::invoke(api::Solver* solver, } Command* EchoCommand::clone() const { return new EchoCommand(d_output); } + std::string EchoCommand::getCommandName() const { return "echo"; } void EchoCommand::toStream(std::ostream& out, diff --git a/src/util/smt2_quote_string.cpp b/src/util/smt2_quote_string.cpp index 82750c48b..e2ab4a74c 100644 --- a/src/util/smt2_quote_string.cpp +++ b/src/util/smt2_quote_string.cpp @@ -42,4 +42,16 @@ std::string quoteSymbol(const std::string& s){ return s; } +std::string quoteString(const std::string& s) { + // escape all double-quotes + std::string output = s; + size_t pos = 0; + while ((pos = output.find('"', pos)) != std::string::npos) + { + output.replace(pos, 1, "\"\""); + pos += 2; + } + return '"' + output + '"'; +} + } // namespace cvc5 diff --git a/src/util/smt2_quote_string.h b/src/util/smt2_quote_string.h index 98b2f89dd..f8be53c0c 100644 --- a/src/util/smt2_quote_string.h +++ b/src/util/smt2_quote_string.h @@ -27,6 +27,11 @@ namespace cvc5 { */ std::string quoteSymbol(const std::string& s); +/** + * SMT-LIB 2 quoting for strings + */ +std::string quoteString(const std::string& s); + } // namespace cvc5 #endif /* CVC5__UTIL__SMT2_QUOTE_STRING_H */ -- cgit v1.2.3 From 1c744822538cff4e598b411514c4580848f1517b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 20 Oct 2021 06:57:44 -0500 Subject: Correctly parse uninterpreted constant values in get-value (#7393) SMT-LIB indicates that abstract values can appear in terms as arguments to `get-value`. This is not currently the case, as pointed out by #6908. This updates our parser so that bindings are added to the symbol table for all uninterpreted constants in the model whenever we parse a `get-value` term. Fixes #6908. --- src/parser/parser.cpp | 30 ++++++++++++++++++++++ src/parser/parser.h | 8 ++++++ src/parser/smt2/Smt2.g | 9 ++++++- test/regress/CMakeLists.txt | 1 + .../regress0/parser/issue6908-get-value-uc.smt2 | 10 ++++++++ 5 files changed, 57 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress0/parser/issue6908-get-value-uc.smt2 (limited to 'src') diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 84c0bd17c..9f34b5647 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -737,6 +737,36 @@ void Parser::pushScope(bool isUserContext) d_symman->pushScope(isUserContext); } +void Parser::pushGetValueScope() +{ + pushScope(); + // we must bind all relevant uninterpreted constants, which coincide with + // the set of uninterpreted constants that are printed in the definition + // of a model. + std::vector declareSorts = d_symman->getModelDeclareSorts(); + Trace("parser") << "Push get value scope, with " << declareSorts.size() + << " declared sorts" << std::endl; + for (const api::Sort& s : declareSorts) + { + std::vector elements = d_solver->getModelDomainElements(s); + for (const api::Term& e : elements) + { + // Uninterpreted constants are abstract values, which by SMT-LIB are + // required to be annotated with their type, e.g. (as @uc_Foo_0 Foo). + // Thus, the element is not printed simply as its name. + std::string en = e.toString(); + size_t index = en.find("(as "); + if (index == 0) + { + index = en.find(" ", 4); + en = en.substr(4, index - 4); + } + Trace("parser") << "Get value scope : " << en << " -> " << e << std::endl; + defineVar(en, e); + } + } +} + void Parser::popScope() { d_symman->popScope(); diff --git a/src/parser/parser.h b/src/parser/parser.h index 4b04c77b7..19e5b8531 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -716,6 +716,14 @@ public: */ void pushScope(bool isUserContext = false); + /** Push scope for get-value + * + * This pushes a scope by a call to pushScope that binds all relevant bindings + * required for parsing the SMT-LIB command `get-value`. This includes + * all uninterpreted constant values in user-defined uninterpreted sorts. + */ + void pushGetValueScope(); + void popScope(); virtual void reset(); diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index a75aa36da..e3aee250e 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -343,7 +343,13 @@ command [std::unique_ptr* cmd] | DECLARE_DATATYPE_TOK datatypeDefCommand[false, cmd] | DECLARE_DATATYPES_TOK datatypesDefCommand[false, cmd] | /* value query */ - GET_VALUE_TOK { PARSER_STATE->checkThatLogicIsSet(); } + GET_VALUE_TOK + { + PARSER_STATE->checkThatLogicIsSet(); + // bind all symbols specific to the model, e.g. uninterpreted constant + // values + PARSER_STATE->pushGetValueScope(); + } ( LPAREN_TOK termList[terms,expr] RPAREN_TOK { cmd->reset(new GetValueCommand(terms)); } | ~LPAREN_TOK @@ -352,6 +358,7 @@ command [std::unique_ptr* cmd] "parentheses?"); } ) + { PARSER_STATE->popScope(); } | /* get-assignment */ GET_ASSIGNMENT_TOK { PARSER_STATE->checkThatLogicIsSet(); } { cmd->reset(new GetAssignmentCommand()); } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 81b2bd0c9..da6f4c3c9 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -782,6 +782,7 @@ set(regress_0_tests regress0/parser/force_logic_set_logic.smt2 regress0/parser/force_logic_success.smt2 regress0/parser/issue5163.smt2 + regress0/parser/issue6908-get-value-uc.smt2 regress0/parser/issue7274.smt2 regress0/parser/linear_arithmetic_err1.smt2 regress0/parser/linear_arithmetic_err2.smt2 diff --git a/test/regress/regress0/parser/issue6908-get-value-uc.smt2 b/test/regress/regress0/parser/issue6908-get-value-uc.smt2 new file mode 100644 index 000000000..b6825fe27 --- /dev/null +++ b/test/regress/regress0/parser/issue6908-get-value-uc.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --produce-models +; EXPECT: sat +; EXPECT: (((f (as @uc_Foo_0 Foo)) 3)) +(set-logic ALL) +(set-option :produce-models true) +(declare-sort Foo 0) +(declare-fun f (Foo) Int) +(assert (exists ((x Foo)) (= (f x) 3))) +(check-sat) +(get-value ((f @uc_Foo_0))) -- cgit v1.2.3 From 3e9e1c54ef54627e4f38094910effb32f6ad7cd2 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 20 Oct 2021 09:34:10 -0500 Subject: Do not make assumption about model for Boolean variables in FMF (#7407) Fixes cases where models can be wrong for FMF with Boolean variables in the bodies of quantified formulas. Fixes #6744, all benchmarks on that issue are fixed. This PR adds 2 of the regressions from that issue. --- src/theory/quantifiers/fmf/full_model_check.cpp | 11 ++++++++--- test/regress/CMakeLists.txt | 2 ++ test/regress/regress1/fmf/issue6744-2-unc-bool-var.smt2 | 7 +++++++ test/regress/regress1/fmf/issue6744-3-unc-bool-var.smt2 | 5 +++++ 4 files changed, 22 insertions(+), 3 deletions(-) create mode 100644 test/regress/regress1/fmf/issue6744-2-unc-bool-var.smt2 create mode 100644 test/regress/regress1/fmf/issue6744-3-unc-bool-var.smt2 (limited to 'src') diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index 7c1d36ce8..94351274a 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -951,10 +951,15 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n Node r = n; if( !n.isConst() ){ TypeNode tn = n.getType(); - if( !fm->hasTerm(n) && tn.isFirstClass() ){ - r = getSomeDomainElement(fm, tn ); + if (!fm->hasTerm(n) && tn.isFirstClass()) + { + // if the term is unknown, we do not assume any value for it + r = Node::null(); + } + else + { + r = fm->getRepresentative(r); } - r = fm->getRepresentative( r ); } Trace("fmc-debug") << "Add constant entry..." << std::endl; d.addEntry(fm, mkCondDefault(fm, f), r); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index da6f4c3c9..d24150cf6 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1648,6 +1648,8 @@ set(regress_1_tests regress1/fmf/issue4225-univ-fun.smt2 regress1/fmf/issue5738-dt-interp-finite.smt2 regress1/fmf/issue6690-re-enum.smt2 + regress1/fmf/issue6744-2-unc-bool-var.smt2 + regress1/fmf/issue6744-3-unc-bool-var.smt2 regress1/fmf/issue916-fmf-or.smt2 regress1/fmf/jasmin-cdt-crash.smt2 regress1/fmf/loopy_coda.smt2 diff --git a/test/regress/regress1/fmf/issue6744-2-unc-bool-var.smt2 b/test/regress/regress1/fmf/issue6744-2-unc-bool-var.smt2 new file mode 100644 index 000000000..024d5b6a3 --- /dev/null +++ b/test/regress/regress1/fmf/issue6744-2-unc-bool-var.smt2 @@ -0,0 +1,7 @@ +(set-logic ALL) +(set-option :finite-model-find true) +(set-info :status sat) +(declare-fun v () Bool) +(declare-fun v2 () Bool) +(assert (exists ((q (Array Bool (Array Bool (Array Int Bool))))) (forall ((q3 (Array Bool (Array Bool (Array Int Bool))))) (xor v2 v2 v v2 (or v2 (not (= q3 q))))))) +(check-sat) diff --git a/test/regress/regress1/fmf/issue6744-3-unc-bool-var.smt2 b/test/regress/regress1/fmf/issue6744-3-unc-bool-var.smt2 new file mode 100644 index 000000000..eb0c35f68 --- /dev/null +++ b/test/regress/regress1/fmf/issue6744-3-unc-bool-var.smt2 @@ -0,0 +1,5 @@ +(set-logic UFC) +(set-info :status sat) +(declare-fun v () Bool) +(assert (and (forall ((q Bool)) (not (xor v (exists ((q Bool)) true) (and (not v) (not q))))))) +(check-sat) -- cgit v1.2.3 From b038b34584f37c40a6dc4a476e8f486cf6977b81 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 20 Oct 2021 11:14:50 -0500 Subject: Reimplement support for relational triggers (#7063) This makes relational triggers its own kind of instantiation match generator. Future PRs will delete the code interleaved in the core InstMatchGenerator class for handling relational triggers. This PR also fixes two issues related to how trigger techniques are combined: (1) instantiation match generators that are generated as part of multi-triggers now are properly specialized (using getInstMatchGenerator), (2) there was a bug with auto-generated triggers: when the first auto-generated trigger was generated that was already a user trigger, then we would ignore all other auto-generated triggers. This is work towards finding a solution for the choice.move.hard Facebook benchmark, where relational-triggers appear to be a possible solution. --- src/CMakeLists.txt | 2 + .../quantifiers/ematching/inst_match_generator.cpp | 14 ++- .../ematching/inst_strategy_e_matching.cpp | 41 +++---- .../ematching/relational_match_generator.cpp | 125 +++++++++++++++++++++ .../ematching/relational_match_generator.h | 92 +++++++++++++++ .../quantifiers/ematching/trigger_term_info.cpp | 42 ++++++- .../quantifiers/ematching/trigger_term_info.h | 16 ++- test/regress/CMakeLists.txt | 2 + test/regress/regress0/quantifiers/veqt-delta.smt2 | 8 ++ .../quantifiers/choice-move-delta-relt.smt2 | 6 + 10 files changed, 325 insertions(+), 23 deletions(-) create mode 100644 src/theory/quantifiers/ematching/relational_match_generator.cpp create mode 100644 src/theory/quantifiers/ematching/relational_match_generator.h create mode 100644 test/regress/regress0/quantifiers/veqt-delta.smt2 create mode 100644 test/regress/regress1/quantifiers/choice-move-delta-relt.smt2 (limited to 'src') diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index cde739454..a2b5966e1 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -795,6 +795,8 @@ libcvc5_add_sources( theory/quantifiers/ematching/instantiation_engine.h theory/quantifiers/ematching/pattern_term_selector.cpp theory/quantifiers/ematching/pattern_term_selector.h + theory/quantifiers/ematching/relational_match_generator.cpp + theory/quantifiers/ematching/relational_match_generator.h theory/quantifiers/ematching/trigger.cpp theory/quantifiers/ematching/trigger.h theory/quantifiers/ematching/trigger_database.cpp diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp index d8e3b7950..075299583 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp @@ -23,6 +23,7 @@ #include "theory/quantifiers/ematching/inst_match_generator_multi_linear.h" #include "theory/quantifiers/ematching/inst_match_generator_simple.h" #include "theory/quantifiers/ematching/pattern_term_selector.h" +#include "theory/quantifiers/ematching/relational_match_generator.h" #include "theory/quantifiers/ematching/var_match_generator.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quantifiers_state.h" @@ -618,7 +619,7 @@ InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator( InstMatchGenerator* init; std::map< Node, InstMatchGenerator * >::iterator iti = pat_map_init.find( pats[pCounter] ); if( iti==pat_map_init.end() ){ - init = new InstMatchGenerator(tparent, pats[pCounter]); + init = getInstMatchGenerator(tparent, q, pats[pCounter]); }else{ init = iti->second; } @@ -645,6 +646,7 @@ InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Trigger* tparent, Node q, Node n) { + // maybe variable match generator if (n.getKind() != INST_CONSTANT) { Trace("var-trigger-debug") @@ -672,6 +674,16 @@ InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Trigger* tparent, return vmg; } } + Trace("relational-trigger") + << "Is " << n << " a relational trigger?" << std::endl; + // relational triggers + bool hasPol, pol; + Node lit; + if (TriggerTermInfo::isUsableRelationTrigger(n, hasPol, pol, lit)) + { + Trace("relational-trigger") << "...yes, for literal " << lit << std::endl; + return new RelationalMatchGenerator(tparent, lit, hasPol, pol); + } return new InstMatchGenerator(tparent, n); } diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp index 30be83ecc..fdb0d0db3 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp @@ -339,20 +339,18 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ TriggerDatabase::TR_GET_OLD, d_num_trigger_vars[f]); } - if (tr == nullptr) + // if we generated a trigger above, add it + if (tr != nullptr) { - // did not generate a trigger - continue; - } - addTrigger(tr, f); - if (tr->isMultiTrigger()) - { - // only add a single multi-trigger - continue; + addTrigger(tr, f); + if (tr->isMultiTrigger()) + { + // only add a single multi-trigger + continue; + } } // if we are generating additional triggers... - size_t index = 0; - if (index < patTerms.size()) + if (patTerms.size() > 1) { // check if similar patterns exist, and if so, add them additionally unsigned nqfs_curr = 0; @@ -361,7 +359,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ nqfs_curr = d_quant_rel->getNumQuantifiersForSymbol(patTerms[0].getOperator()); } - index++; + size_t index = 1; bool success = true; while (success && index < patTerms.size() && d_is_single_trigger[patTerms[index]]) @@ -527,16 +525,22 @@ bool InstStrategyAutoGenTriggers::generatePatternTerms(Node f) Trace("auto-gen-trigger-debug") << "...required polarity for " << pat << " is " << rpol << ", eq=" << rpoleq << std::endl; + // Currently, we have ad-hoc treatment for relational triggers that + // are not handled by RelationalMatchGen. + bool isAdHocRelationalTrigger = + TriggerTermInfo::isRelationalTrigger(pat) + && !TriggerTermInfo::isUsableRelationTrigger(pat); if (rpol != 0) { Assert(rpol == 1 || rpol == -1); - if (TriggerTermInfo::isRelationalTrigger(pat)) + if (isAdHocRelationalTrigger) { pat = rpol == -1 ? pat.negate() : pat; } else { - Assert(TriggerTermInfo::isAtomicTrigger(pat)); + Assert(TriggerTermInfo::isAtomicTrigger(pat) + || TriggerTermInfo::isUsableRelationTrigger(pat)); if (pat.getType().isBoolean() && rpoleq.isNull()) { if (options().quantifiers.literalMatchMode @@ -575,13 +579,10 @@ bool InstStrategyAutoGenTriggers::generatePatternTerms(Node f) } Trace("auto-gen-trigger-debug") << "...got : " << pat << std::endl; } - else + else if (isAdHocRelationalTrigger) { - if (TriggerTermInfo::isRelationalTrigger(pat)) - { - // consider both polarities - addPatternToPool(f, pat.negate(), num_fv, mpat); - } + // consider both polarities + addPatternToPool(f, pat.negate(), num_fv, mpat); } addPatternToPool(f, pat, num_fv, mpat); } diff --git a/src/theory/quantifiers/ematching/relational_match_generator.cpp b/src/theory/quantifiers/ematching/relational_match_generator.cpp new file mode 100644 index 000000000..8981a7a2d --- /dev/null +++ b/src/theory/quantifiers/ematching/relational_match_generator.cpp @@ -0,0 +1,125 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Relational match generator class. + */ + +#include "theory/quantifiers/ematching/relational_match_generator.h" + +#include "theory/quantifiers/term_util.h" +#include "util/rational.h" + +using namespace cvc5::kind; + +namespace cvc5 { +namespace theory { +namespace quantifiers { +namespace inst { + +RelationalMatchGenerator::RelationalMatchGenerator(Trigger* tparent, + Node rtrigger, + bool hasPol, + bool pol) + : InstMatchGenerator(tparent, Node::null()), + d_vindex(-1), + d_hasPol(hasPol), + d_pol(pol), + d_counter(0) +{ + Assert((rtrigger.getKind() == EQUAL && rtrigger[0].getType().isReal()) + || rtrigger.getKind() == GEQ); + Trace("relational-match-gen") + << "Relational trigger: " << rtrigger << ", hasPol/pol = " << hasPol + << "/" << pol << std::endl; + for (size_t i = 0; i < 2; i++) + { + if (rtrigger[i].getKind() == INST_CONSTANT) + { + d_var = rtrigger[i]; + d_vindex = d_var.getAttribute(InstVarNumAttribute()); + d_rhs = rtrigger[1 - i]; + Assert(!quantifiers::TermUtil::hasInstConstAttr(d_rhs)); + Kind k = rtrigger.getKind(); + d_rel = (i == 0 ? k : (k == GEQ ? LEQ : k)); + break; + } + } + Trace("relational-match-gen") << "...processed " << d_var << " (" << d_vindex + << ") " << d_rel << " " << d_rhs << std::endl; + AlwaysAssert(!d_var.isNull()) + << "Failed to initialize RelationalMatchGenerator"; +} + +bool RelationalMatchGenerator::reset(Node eqc) +{ + d_counter = 0; + return true; +} + +int RelationalMatchGenerator::getNextMatch(Node q, InstMatch& m) +{ + Trace("relational-match-gen") << "getNextMatch, rel match gen" << std::endl; + // try (up to) two different terms + Node s; + Node rhs = d_rhs; + bool rmPrev = m.get(d_vindex).isNull(); + while (d_counter < 2) + { + bool checkPol = false; + if (d_counter == 0) + { + checkPol = d_pol; + } + else + { + Assert(d_counter == 1); + if (d_hasPol) + { + break; + } + // try the opposite polarity + checkPol = !d_pol; + } + NodeManager* nm = NodeManager::currentNM(); + // falsify ( d_var d_rhs ) = checkPol + s = rhs; + if (!checkPol) + { + s = nm->mkNode(PLUS, s, nm->mkConst(Rational(d_rel == GEQ ? -1 : 1))); + } + d_counter++; + Trace("relational-match-gen") + << "...try set " << s << " for " << checkPol << std::endl; + if (m.set(d_qstate, d_vindex, s)) + { + Trace("relational-match-gen") << "...success" << std::endl; + int ret = continueNextMatch(q, m, InferenceId::UNKNOWN); + if (ret > 0) + { + Trace("relational-match-gen") << "...returned " << ret << std::endl; + return ret; + } + Trace("relational-match-gen") << "...failed to gen inst" << std::endl; + // failed + if (rmPrev) + { + m.d_vals[d_vindex] = Node::null(); + } + } + } + return -1; +} + +} // namespace inst +} // namespace quantifiers +} // namespace theory +} // namespace cvc5 diff --git a/src/theory/quantifiers/ematching/relational_match_generator.h b/src/theory/quantifiers/ematching/relational_match_generator.h new file mode 100644 index 000000000..eead2876a --- /dev/null +++ b/src/theory/quantifiers/ematching/relational_match_generator.h @@ -0,0 +1,92 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Relational match generator class. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__THEORY__QUANTIFIERS__RELATIONAL_MATCH_GENERATOR_H +#define CVC5__THEORY__QUANTIFIERS__RELATIONAL_MATCH_GENERATOR_H + +#include "expr/node.h" +#include "theory/quantifiers/ematching/inst_match_generator.h" + +namespace cvc5 { +namespace theory { +namespace quantifiers { +namespace inst { + +/** + * Match generator for relational triggers x ~ t where t is a ground term. + * This match generator tries a small fixed set of terms based on the kind of + * relation and the required polarity of the trigger in the quantified formula. + * + * For example, for quantified formula (forall ((x Int)) (=> (> x n) (P x))), + * we have that (> x n) is a relational trigger with required polarity "true". + * This generator will try the match `x -> n+1` only, where notice that n+1 is + * the canonical term chosen to satisfy x>n. Canonical terms for arithmetic + * relations (~ x n) are in set { n, n+1, n-1 }. + * + * If a relational trigger does not have a required polarity, then up to 2 + * terms are tried, a term that satisfies the relation, and one that does not. + * If (>= x n) is a relational trigger with no polarity, then `x -> n` and + * `x -> n-1` will be generated. + * + * Currently this class handles only equality between real or integer valued + * terms, or inequalities (kind GEQ). It furthermore only considers ground terms + * t for the right hand side of relations. + */ +class RelationalMatchGenerator : public InstMatchGenerator +{ + public: + /** + * @param tparent The parent trigger that this match generator belongs to + * @param rtrigger The relational trigger + * @param hasPol Whether the trigger has an entailed polarity + * @param pol The entailed polarity of the relational trigger. + */ + RelationalMatchGenerator(Trigger* tparent, + Node rtrigger, + bool hasPol, + bool pol); + + /** Reset */ + bool reset(Node eqc) override; + /** Get the next match. */ + int getNextMatch(Node q, InstMatch& m) override; + + private: + /** the variable */ + Node d_var; + /** The index of the variable */ + int64_t d_vindex; + /** the relation kind */ + Kind d_rel; + /** the right hand side */ + Node d_rhs; + /** whether we have a required polarity */ + bool d_hasPol; + /** the required polarity, if it exists */ + bool d_pol; + /** + * The current number of terms we have generated since the last call to reset + */ + size_t d_counter; +}; + +} // namespace inst +} // namespace quantifiers +} // namespace theory +} // namespace cvc5 + +#endif diff --git a/src/theory/quantifiers/ematching/trigger_term_info.cpp b/src/theory/quantifiers/ematching/trigger_term_info.cpp index 600797f4e..f31ec088a 100644 --- a/src/theory/quantifiers/ematching/trigger_term_info.cpp +++ b/src/theory/quantifiers/ematching/trigger_term_info.cpp @@ -70,6 +70,46 @@ bool TriggerTermInfo::isRelationalTriggerKind(Kind k) return k == EQUAL || k == GEQ; } +bool TriggerTermInfo::isUsableRelationTrigger(Node n) +{ + bool hasPol, pol; + Node lit; + return isUsableRelationTrigger(n, hasPol, pol, lit); +} +bool TriggerTermInfo::isUsableRelationTrigger(Node n, + bool& hasPol, + bool& pol, + Node& lit) +{ + // relational triggers (not) (= (~ x t) true|false), where ~ in { =, >= }. + hasPol = false; + pol = n.getKind() != NOT; + lit = pol ? n : n[0]; + if (lit.getKind() == EQUAL && lit[1].getType().isBoolean() + && lit[1].isConst()) + { + hasPol = true; + pol = lit[1].getConst() ? pol : !pol; + lit = lit[0]; + } + // is it a relational trigger? + if ((lit.getKind() == EQUAL && lit[0].getType().isReal()) + || lit.getKind() == GEQ) + { + // if one side of the relation is a variable and the other side is a ground + // term, we can treat this using the relational match generator + for (size_t i = 0; i < 2; i++) + { + if (lit[i].getKind() == INST_CONSTANT + && !quantifiers::TermUtil::hasInstConstAttr(lit[1 - i])) + { + return true; + } + } + } + return false; +} + bool TriggerTermInfo::isSimpleTrigger(Node n) { Node t = n.getKind() == NOT ? n[0] : n; @@ -105,7 +145,7 @@ int32_t TriggerTermInfo::getTriggerWeight(Node n) { return 0; } - if (isAtomicTrigger(n)) + if (isAtomicTrigger(n) || isUsableRelationTrigger(n)) { return 1; } diff --git a/src/theory/quantifiers/ematching/trigger_term_info.h b/src/theory/quantifiers/ematching/trigger_term_info.h index 753d0850c..3816d0988 100644 --- a/src/theory/quantifiers/ematching/trigger_term_info.h +++ b/src/theory/quantifiers/ematching/trigger_term_info.h @@ -108,6 +108,19 @@ class TriggerTermInfo static bool isRelationalTrigger(Node n); /** Is k a relational trigger kind? */ static bool isRelationalTriggerKind(Kind k); + /** + * Is n a usable relational trigger, which is true if RelationalMatchGenerator + * can process n. + */ + static bool isUsableRelationTrigger(Node n); + /** + * Same as above, but lit / hasPol / pol are updated to the required + * constructor arguments for RelationalMatchGenerator. + */ + static bool isUsableRelationTrigger(Node n, + bool& hasPol, + bool& pol, + Node& lit); /** is n a simple trigger (see inst_match_generator.h)? */ static bool isSimpleTrigger(Node n); /** get trigger weight @@ -116,7 +129,8 @@ class TriggerTermInfo * trigger term n, where the smaller the value, the easier. * * Returns 0 for triggers that are APPLY_UF terms. - * Returns 1 for other triggers whose kind is atomic. + * Returns 1 for other triggers whose kind is atomic, or are usable + * relational triggers. * Returns 2 otherwise. */ static int32_t getTriggerWeight(Node n); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index d24150cf6..6dafe6852 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -971,6 +971,7 @@ set(regress_0_tests regress0/quantifiers/simp-len.smt2 regress0/quantifiers/simp-typ-test.smt2 regress0/quantifiers/ufnia-fv-delta.smt2 + regress0/quantifiers/veqt-delta.smt2 regress0/rec-fun-const-parse-bug.smt2 regress0/rels/addr_book_0.cvc.smt2 regress0/rels/atom_univ2.cvc.smt2 @@ -1857,6 +1858,7 @@ set(regress_1_tests regress1/quantifiers/cee-npnt-dd.smt2 regress1/quantifiers/cee-os-delta.smt2 regress1/quantifiers/cdt-0208-to.smt2 + regress1/quantifiers/choice-move-delta-relt.smt2 regress1/quantifiers/const.cvc.smt2 regress1/quantifiers/constfunc.cvc.smt2 regress1/quantifiers/ddatv-delta2.smt2 diff --git a/test/regress/regress0/quantifiers/veqt-delta.smt2 b/test/regress/regress0/quantifiers/veqt-delta.smt2 new file mode 100644 index 000000000..dfac015c6 --- /dev/null +++ b/test/regress/regress0/quantifiers/veqt-delta.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --relational-triggers +; EXPECT: unsat +(set-logic ALL) +(declare-sort S 0) +(declare-fun f () S) +(assert (forall ((? S)) (= ? f))) +(assert (exists ((? S) (v S)) (distinct ? v))) +(check-sat) diff --git a/test/regress/regress1/quantifiers/choice-move-delta-relt.smt2 b/test/regress/regress1/quantifiers/choice-move-delta-relt.smt2 new file mode 100644 index 000000000..a8fd0d498 --- /dev/null +++ b/test/regress/regress1/quantifiers/choice-move-delta-relt.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --relational-triggers --user-pat=use +; EXPECT: unsat +(set-logic ALL) +(declare-fun F (Int) Bool) +(assert (forall ((v Int)) (! (= (F 0) (< v 0)) :qid |outputbpl.194:24| :pattern ((F 0))))) +(check-sat) -- cgit v1.2.3 From 90e615eb3920bd60173e967c85cbcaf4f34a032c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 20 Oct 2021 11:49:53 -0500 Subject: Use codatatype bound variables for codatatype values (#7425) Previously, we had conflated codatatype bound variables and uninterpreted constants (as they have the same functionality). However, we should separate these concepts so we can ensure that uninterpreted constants are only used for uninterpreted sorts. --- src/expr/CMakeLists.txt | 2 + src/expr/codatatype_bound_variable.cpp | 113 +++++++++++++++++++++ src/expr/codatatype_bound_variable.h | 91 +++++++++++++++++ src/expr/uninterpreted_constant.cpp | 6 +- src/theory/datatypes/datatypes_rewriter.cpp | 10 +- src/theory/datatypes/kinds | 9 ++ src/theory/datatypes/theory_datatypes.cpp | 8 +- .../datatypes/theory_datatypes_type_rules.cpp | 8 ++ src/theory/datatypes/theory_datatypes_type_rules.h | 6 ++ src/theory/datatypes/type_enumerator.cpp | 5 +- src/theory/theory_model_builder.cpp | 2 +- test/python/unit/api/test_solver.py | 9 -- test/unit/api/solver_black.cpp | 9 -- 13 files changed, 247 insertions(+), 31 deletions(-) create mode 100644 src/expr/codatatype_bound_variable.cpp create mode 100644 src/expr/codatatype_bound_variable.h (limited to 'src') diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index e73960676..467500868 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -26,6 +26,8 @@ libcvc5_add_sources( bound_var_manager.h cardinality_constraint.cpp cardinality_constraint.h + codatatype_bound_variable.cpp + codatatype_bound_variable.h emptyset.cpp emptyset.h emptybag.cpp diff --git a/src/expr/codatatype_bound_variable.cpp b/src/expr/codatatype_bound_variable.cpp new file mode 100644 index 000000000..a6a9d8e3e --- /dev/null +++ b/src/expr/codatatype_bound_variable.cpp @@ -0,0 +1,113 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Representation of bound variables in codatatype values + */ + +#include "expr/codatatype_bound_variable.h" + +#include +#include +#include +#include + +#include "base/check.h" +#include "expr/type_node.h" + +using namespace std; + +namespace cvc5 { + +CodatatypeBoundVariable::CodatatypeBoundVariable(const TypeNode& type, + Integer index) + : d_type(new TypeNode(type)), d_index(index) +{ + PrettyCheckArgument(type.isCodatatype(), + type, + "codatatype bound variables can only be created for " + "codatatype sorts, not `%s'", + type.toString().c_str()); + PrettyCheckArgument( + index >= 0, + index, + "index >= 0 required for codatatype bound variable index, not `%s'", + index.toString().c_str()); +} + +CodatatypeBoundVariable::~CodatatypeBoundVariable() {} + +CodatatypeBoundVariable::CodatatypeBoundVariable( + const CodatatypeBoundVariable& other) + : d_type(new TypeNode(other.getType())), d_index(other.getIndex()) +{ +} + +const TypeNode& CodatatypeBoundVariable::getType() const { return *d_type; } +const Integer& CodatatypeBoundVariable::getIndex() const { return d_index; } +bool CodatatypeBoundVariable::operator==( + const CodatatypeBoundVariable& cbv) const +{ + return getType() == cbv.getType() && d_index == cbv.d_index; +} +bool CodatatypeBoundVariable::operator!=( + const CodatatypeBoundVariable& cbv) const +{ + return !(*this == cbv); +} + +bool CodatatypeBoundVariable::operator<( + const CodatatypeBoundVariable& cbv) const +{ + return getType() < cbv.getType() + || (getType() == cbv.getType() && d_index < cbv.d_index); +} +bool CodatatypeBoundVariable::operator<=( + const CodatatypeBoundVariable& cbv) const +{ + return getType() < cbv.getType() + || (getType() == cbv.getType() && d_index <= cbv.d_index); +} +bool CodatatypeBoundVariable::operator>( + const CodatatypeBoundVariable& cbv) const +{ + return !(*this <= cbv); +} +bool CodatatypeBoundVariable::operator>=( + const CodatatypeBoundVariable& cbv) const +{ + return !(*this < cbv); +} + +std::ostream& operator<<(std::ostream& out, const CodatatypeBoundVariable& cbv) +{ + std::stringstream ss; + ss << cbv.getType(); + std::string st(ss.str()); + // must remove delimiting quotes from the name of the type + // this prevents us from printing symbols like |@cbv_|T|_n| + std::string q("|"); + size_t pos; + while ((pos = st.find(q)) != std::string::npos) + { + st.replace(pos, 1, ""); + } + return out << "cbv_" << st.c_str() << "_" << cbv.getIndex(); +} + +size_t CodatatypeBoundVariableHashFunction::operator()( + const CodatatypeBoundVariable& cbv) const +{ + return std::hash()(cbv.getType()) + * IntegerHashFunction()(cbv.getIndex()); +} + +} // namespace cvc5 diff --git a/src/expr/codatatype_bound_variable.h b/src/expr/codatatype_bound_variable.h new file mode 100644 index 000000000..9af8476d5 --- /dev/null +++ b/src/expr/codatatype_bound_variable.h @@ -0,0 +1,91 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Representation of bound variables in codatatype values + */ + +#include "cvc5_public.h" + +#ifndef CVC5__EXPR__CODATATYPE_BOUND_VARIABLE_H +#define CVC5__EXPR__CODATATYPE_BOUND_VARIABLE_H + +#include +#include + +#include "util/integer.h" + +namespace cvc5 { + +class TypeNode; + +/** + * In theory, codatatype values are represented in using a MU-notation form, + * where recursive values may contain free constants indexed by their de Bruijn + * indices. This is sometimes written: + * MU x. (cons 0 x). + * where the MU binder is label for a term position, which x references. + * Instead of constructing an explicit MU binder (which is problematic for + * canonicity), we use de Bruijn indices for representing bound variables, + * whose index indicates the level in which it is nested. For example, we + * represent the above value as: + * (cons 0 @cbv_0) + * In the above value, @cbv_0 is a pointer to its direct parent, so the above + * value represents the infinite list (cons 0 (cons 0 (cons 0 ... ))). + * Another example, the value: + * (cons 0 (cons 1 @cbv_1)) + * @cbv_1 is pointer to the top most node of this value, so this is value + * represents the infinite list (cons 0 (cons 1 (cons 0 (cons 1 ...)))). The + * value: + * (cons 0 (cons 1 @cbv_0)) + * on the other hand represents the lasso: + * (cons 0 (cons 1 (cons 1 (cons 1 ... )))) + * + * This class is used for representing the indexed bound variables in the above + * values. It is considered a constant (isConst is true). However, constants + * of codatatype type are normalized by the rewriter (see datatypes rewriter + * normalizeCodatatypeConstant) to ensure their canonicity, via a variant + * of Hopcroft's algorithm. + */ +class CodatatypeBoundVariable +{ + public: + CodatatypeBoundVariable(const TypeNode& type, Integer index); + ~CodatatypeBoundVariable(); + + CodatatypeBoundVariable(const CodatatypeBoundVariable& other); + + const TypeNode& getType() const; + const Integer& getIndex() const; + bool operator==(const CodatatypeBoundVariable& cbv) const; + bool operator!=(const CodatatypeBoundVariable& cbv) const; + bool operator<(const CodatatypeBoundVariable& cbv) const; + bool operator<=(const CodatatypeBoundVariable& cbv) const; + bool operator>(const CodatatypeBoundVariable& cbv) const; + bool operator>=(const CodatatypeBoundVariable& cbv) const; + + private: + std::unique_ptr d_type; + const Integer d_index; +}; +std::ostream& operator<<(std::ostream& out, const CodatatypeBoundVariable& cbv); + +/** + * Hash function for codatatype bound variables. + */ +struct CodatatypeBoundVariableHashFunction +{ + size_t operator()(const CodatatypeBoundVariable& cbv) const; +}; + +} // namespace cvc5 + +#endif /* CVC5__UNINTERPRETED_CONSTANT_H */ diff --git a/src/expr/uninterpreted_constant.cpp b/src/expr/uninterpreted_constant.cpp index ef354568d..709ec112f 100644 --- a/src/expr/uninterpreted_constant.cpp +++ b/src/expr/uninterpreted_constant.cpp @@ -31,7 +31,11 @@ UninterpretedConstant::UninterpretedConstant(const TypeNode& type, Integer index) : d_type(new TypeNode(type)), d_index(index) { - //PrettyCheckArgument(type.isSort(), type, "uninterpreted constants can only be created for uninterpreted sorts, not `%s'", type.toString().c_str()); + PrettyCheckArgument(type.isSort(), + type, + "uninterpreted constants can only be created for " + "uninterpreted sorts, not `%s'", + type.toString().c_str()); PrettyCheckArgument(index >= 0, index, "index >= 0 required for uninterpreted constant index, not `%s'", index.toString().c_str()); } diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp index c446504fd..fd957baaa 100644 --- a/src/theory/datatypes/datatypes_rewriter.cpp +++ b/src/theory/datatypes/datatypes_rewriter.cpp @@ -16,12 +16,12 @@ #include "theory/datatypes/datatypes_rewriter.h" #include "expr/ascription_type.h" +#include "expr/codatatype_bound_variable.h" #include "expr/dtype.h" #include "expr/dtype_cons.h" #include "expr/node_algorithm.h" #include "expr/skolem_manager.h" #include "expr/sygus_datatype.h" -#include "expr/uninterpreted_constant.h" #include "options/datatypes_options.h" #include "theory/datatypes/sygus_datatype_utils.h" #include "theory/datatypes/theory_datatypes_utils.h" @@ -729,7 +729,7 @@ Node DatatypesRewriter::collectRef(Node n, else { // a loop - const Integer& i = n.getConst().getIndex(); + const Integer& i = n.getConst().getIndex(); uint32_t index = i.toUnsignedInt(); if (index >= sk.size()) { @@ -771,7 +771,7 @@ Node DatatypesRewriter::normalizeCodatatypeConstantEqc( { int debruijn = depth - it->second - 1; return NodeManager::currentNM()->mkConst( - UninterpretedConstant(n.getType(), debruijn)); + CodatatypeBoundVariable(n.getType(), debruijn)); } std::vector children; bool childChanged = false; @@ -798,10 +798,10 @@ Node DatatypesRewriter::replaceDebruijn(Node n, TypeNode orig_tn, unsigned depth) { - if (n.getKind() == kind::UNINTERPRETED_CONSTANT && n.getType() == orig_tn) + if (n.getKind() == kind::CODATATYPE_BOUND_VARIABLE && n.getType() == orig_tn) { unsigned index = - n.getConst().getIndex().toUnsignedInt(); + n.getConst().getIndex().toUnsignedInt(); if (index == depth) { return orig; diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds index 41d5ded76..cb3a78cf2 100644 --- a/src/theory/datatypes/kinds +++ b/src/theory/datatypes/kinds @@ -145,4 +145,13 @@ parameterized TUPLE_PROJECT TUPLE_PROJECT_OP 1 \ typerule TUPLE_PROJECT_OP "SimpleTypeRule" typerule TUPLE_PROJECT ::cvc5::theory::datatypes::TupleProjectTypeRule +# For representing codatatype values +constant CODATATYPE_BOUND_VARIABLE \ + class \ + CodatatypeBoundVariable \ + ::cvc5::CodatatypeBoundVariableHashFunction \ + "expr/codatatype_bound_variable.h" \ + "the kind of expressions representing bound variables in codatatype constants, which are de Bruijn indexed variables; payload is an instance of the cvc5::CodatatypeBoundVariable class (used in models)" +typerule CODATATYPE_BOUND_VARIABLE ::cvc5::theory::datatypes::CodatatypeBoundVariableTypeRule + endtheory diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index c892ffc11..0cbeaa515 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -18,11 +18,11 @@ #include #include "base/check.h" +#include "expr/codatatype_bound_variable.h" #include "expr/dtype.h" #include "expr/dtype_cons.h" #include "expr/kind.h" #include "expr/skolem_manager.h" -#include "expr/uninterpreted_constant.h" #include "options/datatypes_options.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" @@ -1290,10 +1290,10 @@ bool TheoryDatatypes::collectModelValues(TheoryModel* m, Node TheoryDatatypes::getCodatatypesValue( Node n, std::map< Node, Node >& eqc_cons, std::map< Node, int >& vmap, int depth ){ std::map< Node, int >::iterator itv = vmap.find( n ); + NodeManager* nm = NodeManager::currentNM(); if( itv!=vmap.end() ){ int debruijn = depth - 1 - itv->second; - return NodeManager::currentNM()->mkConst( - UninterpretedConstant(n.getType(), debruijn)); + return nm->mkConst(CodatatypeBoundVariable(n.getType(), debruijn)); }else if( n.getType().isDatatype() ){ Node nc = eqc_cons[n]; if( !nc.isNull() ){ @@ -1308,7 +1308,7 @@ Node TheoryDatatypes::getCodatatypesValue( Node n, std::map< Node, Node >& eqc_c children.push_back( rv ); } vmap.erase( n ); - return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children ); + return nm->mkNode(APPLY_CONSTRUCTOR, children); } } return n; diff --git a/src/theory/datatypes/theory_datatypes_type_rules.cpp b/src/theory/datatypes/theory_datatypes_type_rules.cpp index 503eaf4df..86a11357b 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.cpp +++ b/src/theory/datatypes/theory_datatypes_type_rules.cpp @@ -18,6 +18,7 @@ #include #include "expr/ascription_type.h" +#include "expr/codatatype_bound_variable.h" #include "expr/dtype.h" #include "expr/dtype_cons.h" #include "expr/type_matcher.h" @@ -597,6 +598,13 @@ TypeNode TupleProjectTypeRule::computeType(NodeManager* nm, TNode n, bool check) return nm->mkTupleType(types); } +TypeNode CodatatypeBoundVariableTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) +{ + return n.getConst().getType(); +} + } // namespace datatypes } // namespace theory } // namespace cvc5 diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index cf57a6c0d..7cf98aa74 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -99,6 +99,12 @@ class TupleProjectTypeRule static TypeNode computeType(NodeManager* nm, TNode n, bool check); }; +class CodatatypeBoundVariableTypeRule +{ + public: + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); +}; + } // namespace datatypes } // namespace theory } // namespace cvc5 diff --git a/src/theory/datatypes/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp index 39b48ece9..6528f1052 100644 --- a/src/theory/datatypes/type_enumerator.cpp +++ b/src/theory/datatypes/type_enumerator.cpp @@ -16,6 +16,7 @@ #include "theory/datatypes/type_enumerator.h" #include "expr/ascription_type.h" +#include "expr/codatatype_bound_variable.h" #include "expr/dtype_cons.h" #include "theory/datatypes/datatypes_rewriter.h" #include "theory/datatypes/theory_datatypes_utils.h" @@ -108,8 +109,8 @@ Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){ { if (d_child_enum) { - ret = NodeManager::currentNM()->mkConst( - UninterpretedConstant(d_type, d_size_limit)); + NodeManager* nm = NodeManager::currentNM(); + ret = nm->mkConst(CodatatypeBoundVariable(d_type, d_size_limit)); } else { diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index 33dbe9ffa..1a0549a0a 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -224,7 +224,7 @@ bool TheoryEngineModelBuilder::isExcludedCdtValue( { Trace("model-builder-debug") << " ...matches with " << eqc << " -> " << eqc_m << std::endl; - if (eqc_m.getKind() == kind::UNINTERPRETED_CONSTANT) + if (eqc_m.getKind() == kind::CODATATYPE_BOUND_VARIABLE) { Trace("model-builder-debug") << "*** " << val << " is excluded datatype for " << eqc diff --git a/test/python/unit/api/test_solver.py b/test/python/unit/api/test_solver.py index db49f8bea..29d637dc6 100644 --- a/test/python/unit/api/test_solver.py +++ b/test/python/unit/api/test_solver.py @@ -381,15 +381,6 @@ def test_mk_rounding_mode(solver): solver.mkRoundingMode(pycvc5.RoundTowardZero) -def test_mk_uninterpreted_const(solver): - solver.mkUninterpretedConst(solver.getBooleanSort(), 1) - with pytest.raises(RuntimeError): - solver.mkUninterpretedConst(pycvc5.Sort(solver), 1) - slv = pycvc5.Solver() - with pytest.raises(RuntimeError): - slv.mkUninterpretedConst(solver.getBooleanSort(), 1) - - def test_mk_abstract_value(solver): solver.mkAbstractValue("1") with pytest.raises(ValueError): diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp index 19113ae13..f90018101 100644 --- a/test/unit/api/solver_black.cpp +++ b/test/unit/api/solver_black.cpp @@ -376,15 +376,6 @@ TEST_F(TestApiBlackSolver, mkRoundingMode) ASSERT_NO_THROW(d_solver.mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO)); } -TEST_F(TestApiBlackSolver, mkUninterpretedConst) -{ - ASSERT_NO_THROW(d_solver.mkUninterpretedConst(d_solver.getBooleanSort(), 1)); - ASSERT_THROW(d_solver.mkUninterpretedConst(Sort(), 1), CVC5ApiException); - Solver slv; - ASSERT_THROW(slv.mkUninterpretedConst(d_solver.getBooleanSort(), 1), - CVC5ApiException); -} - TEST_F(TestApiBlackSolver, mkAbstractValue) { ASSERT_NO_THROW(d_solver.mkAbstractValue(std::string("1"))); -- cgit v1.2.3 From 5f97877e517f024f6d44d3201f5214853d04cc26 Mon Sep 17 00:00:00 2001 From: Lachnitt Date: Wed, 20 Oct 2021 11:50:38 -0700 Subject: [proofs] Alethe: Documentation on Translation (#7394) Provides background on the translation into the Alethe calculus that is common to all rules. Co-authored-by: Haniel Barbosa --- src/proof/alethe/alethe_post_processor.cpp | 73 ++++++++++++++++++++++++++++++ 1 file changed, 73 insertions(+) (limited to 'src') diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp index 6312f3140..ef7735b44 100644 --- a/src/proof/alethe/alethe_post_processor.cpp +++ b/src/proof/alethe/alethe_post_processor.cpp @@ -55,6 +55,79 @@ bool AletheProofPostprocessCallback::update(Node res, switch (id) { + // To keep the original shape of the proof node it is necessary to rederive + // the original conclusion. However, the term that should be printed might + // be different from that conclusion. Thus, it is stored as an additional + // argument in the proof node. Usually, the only difference is an additional + // cl operator or the outmost or operator being replaced by a cl operator. + // + // When steps are added to the proof that have not been there previously, + // it is unwise to add them in the same manner. To illustrate this the + // following counterexample shows the pitfalls of this approach: + // + // (or a (or b c)) (not a) + // --------------------------- RESOLUTION + // (or b c) + // + // is converted into an Alethe proof that should be printed as + // + // (cl a (or b c)) (cl (not a)) + // -------------------------------- RESOLUTION + // (cl (or b c)) + // --------------- OR + // (cl b c) + // + // Here, (cl (or b c)) and (cl b c) cannot correspond to the same proof node + // (or b c). Thus, we build a new proof node using the kind SEXPR + // that is then printed as (cl (or b c)). We denote this wrapping of a proof + // node by using an extra pair of parenthesis, i.e. ((or b c)) is the proof + // node printed as (cl (or b c)). + // + // + // Some proof rules have a close correspondence in Alethe. There are two + // very frequent patterns that, to avoid repetition, are described here and + // referred to in the comments on the specific proof rules below. + // + // The first pattern, which will be called singleton pattern in the + // following, adds the original proof node F with the corresponding rule R' + // of the Alethe calculus and uses the same premises as the original proof + // node (P1:F1) ... (Pn:Fn). However, the conclusion is printed as (cl F). + // + // This means a cvc5 rule R that looks as follows: + // + // (P1:F1) ... (Pn:Fn) + // --------------------- R + // F + // + // is transformed into: + // + // (P1:F1) ... (Pn:Fn) + // --------------------- R' + // (cl F)* + // + // * the corresponding proof node is F + // + // The second pattern, which will be called clause pattern in the following, + // has a disjunction (or G1 ... Gn) as conclusion. It also adds the orignal + // proof node (or G1 ... Gn) with the corresponding rule R' of the Alethe + // calculus and uses the same premises as the original proof node (P1:F1) + // ... (Pn:Fn). However, the conclusion is printed as (cl G1 ... Gn), i.e. + // the or is replaced by the cl operator. + // + // This means a cvc5 rule R that looks as follows: + // + // (P1:F1) ... (Pn:Fn) + // --------------------- R + // (or G1 ... Gn) + // + // Is transformed into: + // + // (P1:F1) ... (Pn:Fn) + // --------------------- R' + // (cl G1 ... Gn)* + // + // * the corresponding proof node is (or G1 ... Gn) + // //================================================= Core rules //======================== Assume and Scope case PfRule::ASSUME: -- cgit v1.2.3 From 68fc65dfb303d75eab953523744103ba2b65ac8e Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 20 Oct 2021 12:14:59 -0700 Subject: api: Rename get(BV|FP)*Size functions for consistency. (#7428) --- src/api/cpp/cvc5.cpp | 11 ++++++----- src/api/cpp/cvc5.h | 6 +++--- src/api/java/cvc5/Sort.java | 18 +++++++++--------- src/api/java/jni/cvc5_Sort.cpp | 28 +++++++++++++--------------- src/api/python/cvc5.pxd | 6 +++--- src/api/python/cvc5.pxi | 12 ++++++------ test/api/issue6111.cpp | 2 +- test/python/unit/api/test_sort.py | 12 ++++++------ test/unit/api/java/cvc5/SortTest.java | 18 +++++++++--------- test/unit/api/sort_black.cpp | 18 +++++++++--------- 10 files changed, 65 insertions(+), 66 deletions(-) (limited to 'src') diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 778f700c0..f6a1eed17 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -1682,7 +1682,7 @@ size_t Sort::getSortConstructorArity() const /* Bit-vector sort ----------------------------------------------------- */ -uint32_t Sort::getBVSize() const +uint32_t Sort::getBitVectorSize() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; @@ -1695,7 +1695,7 @@ uint32_t Sort::getBVSize() const /* Floating-point sort ------------------------------------------------- */ -uint32_t Sort::getFPExponentSize() const +uint32_t Sort::getFloatingPointExponentSize() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; @@ -1706,7 +1706,7 @@ uint32_t Sort::getFPExponentSize() const CVC5_API_TRY_CATCH_END; } -uint32_t Sort::getFPSignificandSize() const +uint32_t Sort::getFloatingPointSignificandSize() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; @@ -6030,10 +6030,11 @@ Term Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const CVC5_API_ARG_CHECK_EXPECTED(exp > 0, exp) << "a value > 0"; CVC5_API_ARG_CHECK_EXPECTED(sig > 0, sig) << "a value > 0"; uint32_t bw = exp + sig; - CVC5_API_ARG_CHECK_EXPECTED(bw == val.getSort().getBVSize(), val) + CVC5_API_ARG_CHECK_EXPECTED(bw == val.d_node->getType().getBitVectorSize(), + val) << "a bit-vector constant with bit-width '" << bw << "'"; CVC5_API_ARG_CHECK_EXPECTED( - val.getSort().isBitVector() && val.d_node->isConst(), val) + val.d_node->getType().isBitVector() && val.d_node->isConst(), val) << "bit-vector constant"; //////// all checks before this line return mkValHelper( diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 5e0f0d834..ded477a9d 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -700,19 +700,19 @@ class CVC5_EXPORT Sort /** * @return the bit-width of the bit-vector sort */ - uint32_t getBVSize() const; + uint32_t getBitVectorSize() const; /* Floating-point sort ------------------------------------------------- */ /** * @return the bit-width of the exponent of the floating-point sort */ - uint32_t getFPExponentSize() const; + uint32_t getFloatingPointExponentSize() const; /** * @return the width of the significand of the floating-point sort */ - uint32_t getFPSignificandSize() const; + uint32_t getFloatingPointSignificandSize() const; /* Datatype sort ------------------------------------------------------- */ diff --git a/src/api/java/cvc5/Sort.java b/src/api/java/cvc5/Sort.java index f1f541e35..434c07424 100644 --- a/src/api/java/cvc5/Sort.java +++ b/src/api/java/cvc5/Sort.java @@ -725,34 +725,34 @@ public class Sort extends AbstractPointer implements Comparable /** * @return the bit-width of the bit-vector sort */ - public int getBVSize() + public int getBitVectorSize() { - return getBVSize(pointer); + return getBitVectorSize(pointer); } - private native int getBVSize(long pointer); + private native int getBitVectorSize(long pointer); /* Floating-point sort ------------------------------------------------- */ /** * @return the bit-width of the exponent of the floating-point sort */ - public int getFPExponentSize() + public int getFloatingPointExponentSize() { - return getFPExponentSize(pointer); + return getFloatingPointExponentSize(pointer); } - private native int getFPExponentSize(long pointer); + private native int getFloatingPointExponentSize(long pointer); /** * @return the width of the significand of the floating-point sort */ - public int getFPSignificandSize() + public int getFloatingPointSignificandSize() { - return getFPSignificandSize(pointer); + return getFloatingPointSignificandSize(pointer); } - private native int getFPSignificandSize(long pointer); + private native int getFloatingPointSignificandSize(long pointer); /* Datatype sort ------------------------------------------------------- */ diff --git a/src/api/java/jni/cvc5_Sort.cpp b/src/api/java/jni/cvc5_Sort.cpp index a2754f032..36ba81249 100644 --- a/src/api/java/jni/cvc5_Sort.cpp +++ b/src/api/java/jni/cvc5_Sort.cpp @@ -978,46 +978,44 @@ JNIEXPORT jint JNICALL Java_cvc5_Sort_getSortConstructorArity(JNIEnv* env, /* * Class: cvc5_Sort - * Method: getBVSize + * Method: getBitVectorSize * Signature: (J)I */ -JNIEXPORT jint JNICALL Java_cvc5_Sort_getBVSize(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jint JNICALL Java_cvc5_Sort_getBitVectorSize(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast(pointer); - return static_cast(current->getBVSize()); + return static_cast(current->getBitVectorSize()); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } /* * Class: cvc5_Sort - * Method: getFPExponentSize + * Method: getFloatingPointExponentSize * Signature: (J)I */ -JNIEXPORT jint JNICALL Java_cvc5_Sort_getFPExponentSize(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jint JNICALL +Java_cvc5_Sort_getFloatingPointExponentSize(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast(pointer); - return static_cast(current->getFPExponentSize()); + return static_cast(current->getFloatingPointExponentSize()); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } /* * Class: cvc5_Sort - * Method: getFPSignificandSize + * Method: getFloatingPointSignificandSize * Signature: (J)I */ -JNIEXPORT jint JNICALL Java_cvc5_Sort_getFPSignificandSize(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jint JNICALL Java_cvc5_Sort_getFloatingPointSignificandSize( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast(pointer); - return static_cast(current->getFPSignificandSize()); + return static_cast(current->getFloatingPointSignificandSize()); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index ef9971c20..08bcc956a 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -357,9 +357,9 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": vector[Sort] getUninterpretedSortParamSorts() except + string getSortConstructorName() except + size_t getSortConstructorArity() except + - uint32_t getBVSize() except + - uint32_t getFPExponentSize() except + - uint32_t getFPSignificandSize() except + + uint32_t getBitVectorSize() except + + uint32_t getFloatingPointExponentSize() except + + uint32_t getFloatingPointSignificandSize() except + vector[Sort] getDatatypeParamSorts() except + size_t getDatatypeArity() except + size_t getTupleLength() except + diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 2a35363ea..6b6d391e6 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -2396,14 +2396,14 @@ cdef class Sort: def getSortConstructorArity(self): return self.csort.getSortConstructorArity() - def getBVSize(self): - return self.csort.getBVSize() + def getBitVectorSize(self): + return self.csort.getBitVectorSize() - def getFPExponentSize(self): - return self.csort.getFPExponentSize() + def getFloatingPointExponentSize(self): + return self.csort.getFloatingPointExponentSize() - def getFPSignificandSize(self): - return self.csort.getFPSignificandSize() + def getFloatingPointSignificandSize(self): + return self.csort.getFloatingPointSignificandSize() def getDatatypeParamSorts(self): param_sorts = [] diff --git a/test/api/issue6111.cpp b/test/api/issue6111.cpp index bd7be2ad0..c0366ce23 100644 --- a/test/api/issue6111.cpp +++ b/test/api/issue6111.cpp @@ -27,7 +27,7 @@ int main() solver.setLogic("QF_BV"); Sort bvsort12979 = solver.mkBitVectorSort(12979); Term input2_1 = solver.mkConst(bvsort12979, "intpu2_1"); - Term zero = solver.mkBitVector(bvsort12979.getBVSize(), "0", 10); + Term zero = solver.mkBitVector(bvsort12979.getBitVectorSize(), "0", 10); vector args1; args1.push_back(zero); diff --git a/test/python/unit/api/test_sort.py b/test/python/unit/api/test_sort.py index def539cf4..db8cbff25 100644 --- a/test/python/unit/api/test_sort.py +++ b/test/python/unit/api/test_sort.py @@ -438,26 +438,26 @@ def test_get_uninterpreted_sort_constructor_arity(solver): def test_get_bv_size(solver): bvSort = solver.mkBitVectorSort(32) - bvSort.getBVSize() + bvSort.getBitVectorSize() setSort = solver.mkSetSort(solver.getIntegerSort()) with pytest.raises(RuntimeError): - setSort.getBVSize() + setSort.getBitVectorSize() def test_get_fp_exponent_size(solver): fpSort = solver.mkFloatingPointSort(4, 8) - fpSort.getFPExponentSize() + fpSort.getFloatingPointExponentSize() setSort = solver.mkSetSort(solver.getIntegerSort()) with pytest.raises(RuntimeError): - setSort.getFPExponentSize() + setSort.getFloatingPointExponentSize() def test_get_fp_significand_size(solver): fpSort = solver.mkFloatingPointSort(4, 8) - fpSort.getFPSignificandSize() + fpSort.getFloatingPointSignificandSize() setSort = solver.mkSetSort(solver.getIntegerSort()) with pytest.raises(RuntimeError): - setSort.getFPSignificandSize() + setSort.getFloatingPointSignificandSize() def test_get_datatype_paramsorts(solver): diff --git a/test/unit/api/java/cvc5/SortTest.java b/test/unit/api/java/cvc5/SortTest.java index f2f9edaed..1ea703268 100644 --- a/test/unit/api/java/cvc5/SortTest.java +++ b/test/unit/api/java/cvc5/SortTest.java @@ -458,28 +458,28 @@ class SortTest assertThrows(CVC5ApiException.class, () -> bvSort.getSortConstructorArity()); } - @Test void getBVSize() throws CVC5ApiException + @Test void getBitVectorSize() throws CVC5ApiException { Sort bvSort = d_solver.mkBitVectorSort(32); - assertDoesNotThrow(() -> bvSort.getBVSize()); + assertDoesNotThrow(() -> bvSort.getBitVectorSize()); Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); - assertThrows(CVC5ApiException.class, () -> setSort.getBVSize()); + assertThrows(CVC5ApiException.class, () -> setSort.getBitVectorSize()); } - @Test void getFPExponentSize() throws CVC5ApiException + @Test void getFloatingPointExponentSize() throws CVC5ApiException { Sort fpSort = d_solver.mkFloatingPointSort(4, 8); - assertDoesNotThrow(() -> fpSort.getFPExponentSize()); + assertDoesNotThrow(() -> fpSort.getFloatingPointExponentSize()); Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); - assertThrows(CVC5ApiException.class, () -> setSort.getFPExponentSize()); + assertThrows(CVC5ApiException.class, () -> setSort.getFloatingPointExponentSize()); } - @Test void getFPSignificandSize() throws CVC5ApiException + @Test void getFloatingPointSignificandSize() throws CVC5ApiException { Sort fpSort = d_solver.mkFloatingPointSort(4, 8); - assertDoesNotThrow(() -> fpSort.getFPSignificandSize()); + assertDoesNotThrow(() -> fpSort.getFloatingPointSignificandSize()); Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); - assertThrows(CVC5ApiException.class, () -> setSort.getFPSignificandSize()); + assertThrows(CVC5ApiException.class, () -> setSort.getFloatingPointSignificandSize()); } @Test void getDatatypeParamSorts() throws CVC5ApiException diff --git a/test/unit/api/sort_black.cpp b/test/unit/api/sort_black.cpp index 757bacad6..1e9505ee1 100644 --- a/test/unit/api/sort_black.cpp +++ b/test/unit/api/sort_black.cpp @@ -470,28 +470,28 @@ TEST_F(TestApiBlackSort, getUninterpretedSortConstructorArity) ASSERT_THROW(bvSort.getSortConstructorArity(), CVC5ApiException); } -TEST_F(TestApiBlackSort, getBVSize) +TEST_F(TestApiBlackSort, getBitVectorSize) { Sort bvSort = d_solver.mkBitVectorSort(32); - ASSERT_NO_THROW(bvSort.getBVSize()); + ASSERT_NO_THROW(bvSort.getBitVectorSize()); Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); - ASSERT_THROW(setSort.getBVSize(), CVC5ApiException); + ASSERT_THROW(setSort.getBitVectorSize(), CVC5ApiException); } -TEST_F(TestApiBlackSort, getFPExponentSize) +TEST_F(TestApiBlackSort, getFloatingPointExponentSize) { Sort fpSort = d_solver.mkFloatingPointSort(4, 8); - ASSERT_NO_THROW(fpSort.getFPExponentSize()); + ASSERT_NO_THROW(fpSort.getFloatingPointExponentSize()); Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); - ASSERT_THROW(setSort.getFPExponentSize(), CVC5ApiException); + ASSERT_THROW(setSort.getFloatingPointExponentSize(), CVC5ApiException); } -TEST_F(TestApiBlackSort, getFPSignificandSize) +TEST_F(TestApiBlackSort, getFloatingPointSignificandSize) { Sort fpSort = d_solver.mkFloatingPointSort(4, 8); - ASSERT_NO_THROW(fpSort.getFPSignificandSize()); + ASSERT_NO_THROW(fpSort.getFloatingPointSignificandSize()); Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); - ASSERT_THROW(setSort.getFPSignificandSize(), CVC5ApiException); + ASSERT_THROW(setSort.getFloatingPointSignificandSize(), CVC5ApiException); } TEST_F(TestApiBlackSort, getDatatypeParamSorts) -- cgit v1.2.3 From 221f8b49844a0d65739393df9327de0338154ff2 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 20 Oct 2021 14:48:11 -0500 Subject: Check whether abduct option is enabled (#7418) This addresses one of the issues related to #6605. --- src/api/cpp/cvc5.cpp | 6 +++++- test/unit/api/solver_black.cpp | 17 +++++++++++++++++ 2 files changed, 22 insertions(+), 1 deletion(-) (limited to 'src') diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index f6a1eed17..2bc101bec 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -7205,7 +7205,7 @@ std::string Solver::getProof(void) const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK(d_slv->getOptions().smt.produceProofs) - << "Cannot get proof explicitly enabled (try --produce-proofs)"; + << "Cannot get proof unless proofs are enabled (try --produce-proofs)"; CVC5_API_RECOVERABLE_CHECK(d_slv->getSmtMode() == SmtMode::UNSAT) << "Cannot get proof unless in unsat mode."; return d_slv->getProof(); @@ -7456,6 +7456,8 @@ bool Solver::getAbduct(const Term& conj, Term& output) const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_TERM(conj); + CVC5_API_CHECK(d_slv->getOptions().smt.produceAbducts) + << "Cannot get abduct unless abducts are enabled (try --produce-abducts)"; //////// all checks before this line Node result; bool success = d_slv->getAbduct(*conj.d_node, result); @@ -7472,6 +7474,8 @@ bool Solver::getAbduct(const Term& conj, Grammar& grammar, Term& output) const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_TERM(conj); + CVC5_API_CHECK(d_slv->getOptions().smt.produceAbducts) + << "Cannot get abduct unless abducts are enabled (try --produce-abducts)"; //////// all checks before this line Node result; bool success = diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp index f90018101..d5137393e 100644 --- a/test/unit/api/solver_black.cpp +++ b/test/unit/api/solver_black.cpp @@ -1225,6 +1225,23 @@ TEST_F(TestApiBlackSolver, getAbduct) ASSERT_EQ(output2, truen); } +TEST_F(TestApiBlackSolver, getAbduct2) +{ + d_solver.setLogic("QF_LIA"); + d_solver.setOption("incremental", "false"); + Sort intSort = d_solver.getIntegerSort(); + Term zero = d_solver.mkInteger(0); + Term x = d_solver.mkConst(intSort, "x"); + Term y = d_solver.mkConst(intSort, "y"); + // Assumptions for abduction: x > 0 + d_solver.assertFormula(d_solver.mkTerm(GT, x, zero)); + // Conjecture for abduction: y > 0 + Term conj = d_solver.mkTerm(GT, y, zero); + Term output; + // Fails due to option not set + ASSERT_THROW(d_solver.getAbduct(conj, output), CVC5ApiException); +} + TEST_F(TestApiBlackSolver, getInterpolant) { d_solver.setLogic("QF_LIA"); -- cgit v1.2.3 From 51e438df97e12b7c893827fe36aca3832e3e1a07 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 20 Oct 2021 15:34:33 -0500 Subject: Do not construct instantiation for checking propagating instantiations spurious (#7390) This makes the check for when an instantiation is "propagating" faster by not constructing the substitution + rewriting of the entire formula, and instead threading the substitution through the entailment check utility's evaluateTerm utility. On a handful of challenge Facebook benchmarks, we go 35 seconds -> 18 seconds with this change. This also eliminates the argument exp to the evaluateTerm method, which is no longer used, and eliminates hasSubs from several methods, which is redundant. --- src/theory/quantifiers/entailment_check.cpp | 156 ++++++++++--------------- src/theory/quantifiers/entailment_check.h | 40 ++++--- src/theory/quantifiers/quant_conflict_find.cpp | 43 +++---- src/theory/quantifiers/quant_conflict_find.h | 2 - 4 files changed, 107 insertions(+), 134 deletions(-) (limited to 'src') diff --git a/src/theory/quantifiers/entailment_check.cpp b/src/theory/quantifiers/entailment_check.cpp index f27e14121..543414a4e 100644 --- a/src/theory/quantifiers/entailment_check.cpp +++ b/src/theory/quantifiers/entailment_check.cpp @@ -33,11 +33,12 @@ EntailmentCheck::EntailmentCheck(Env& env, QuantifiersState& qs, TermDb& tdb) } EntailmentCheck::~EntailmentCheck() {} + Node EntailmentCheck::evaluateTerm2(TNode n, std::map& visited, - std::vector& exp, + std::map& subs, + bool subsRep, bool useEntailmentTests, - bool computeExp, bool reqHasTerm) { std::map::iterator itv = visited.find(n); @@ -45,36 +46,43 @@ Node EntailmentCheck::evaluateTerm2(TNode n, { return itv->second; } - size_t prevSize = exp.size(); Trace("term-db-eval") << "evaluate term : " << n << std::endl; Node ret = n; - if (n.getKind() == FORALL || n.getKind() == BOUND_VARIABLE) + Kind k = n.getKind(); + if (k == FORALL) { // do nothing } - else if (d_qstate.hasTerm(n)) + else if (k == BOUND_VARIABLE) { - Trace("term-db-eval") << "...exists in ee, return rep" << std::endl; - ret = d_qstate.getRepresentative(n); - if (computeExp) + std::map::iterator it = subs.find(n); + if (it != subs.end()) { - if (n != ret) + if (!subsRep) { - exp.push_back(n.eqNode(ret)); + Assert(d_qstate.hasTerm(it->second)); + ret = d_qstate.getRepresentative(it->second); + } + else + { + ret = it->second; } } + } + else if (d_qstate.hasTerm(n)) + { + Trace("term-db-eval") << "...exists in ee, return rep" << std::endl; + ret = d_qstate.getRepresentative(n); reqHasTerm = false; } else if (n.hasOperator()) { std::vector args; bool ret_set = false; - Kind k = n.getKind(); - std::vector tempExp; for (unsigned i = 0, nchild = n.getNumChildren(); i < nchild; i++) { TNode c = evaluateTerm2( - n[i], visited, tempExp, useEntailmentTests, computeExp, reqHasTerm); + n[i], visited, subs, subsRep, useEntailmentTests, reqHasTerm); if (c.isNull()) { ret = Node::null(); @@ -95,32 +103,19 @@ Node EntailmentCheck::evaluateTerm2(TNode n, { ret = evaluateTerm2(n[c == d_true ? 1 : 2], visited, - tempExp, + subs, + subsRep, useEntailmentTests, - computeExp, reqHasTerm); ret_set = true; reqHasTerm = false; break; } } - if (computeExp) - { - exp.insert(exp.end(), tempExp.begin(), tempExp.end()); - } Trace("term-db-eval") << " child " << i << " : " << c << std::endl; args.push_back(c); } - if (ret_set) - { - // if we short circuited - if (computeExp) - { - exp.clear(); - exp.insert(exp.end(), tempExp.begin(), tempExp.end()); - } - } - else + if (!ret_set) { // get the (indexed) operator of n, if it exists TNode f = d_tdb.getMatchOperator(n); @@ -133,29 +128,11 @@ Node EntailmentCheck::evaluateTerm2(TNode n, << " from DB for " << n << std::endl; if (!nn.isNull()) { - if (computeExp) - { - Assert(nn.getNumChildren() == n.getNumChildren()); - for (size_t i = 0, nchild = nn.getNumChildren(); i < nchild; i++) - { - if (nn[i] != n[i]) - { - exp.push_back(nn[i].eqNode(n[i])); - } - } - } ret = d_qstate.getRepresentative(nn); Trace("term-db-eval") << "return rep" << std::endl; ret_set = true; reqHasTerm = false; Assert(!ret.isNull()); - if (computeExp) - { - if (n != ret) - { - exp.push_back(nn.eqNode(ret)); - } - } } } if (!ret_set) @@ -188,10 +165,6 @@ Node EntailmentCheck::evaluateTerm2(TNode n, if (et.first) { ret = j == 0 ? d_true : d_false; - if (computeExp) - { - exp.push_back(et.second); - } break; } } @@ -203,9 +176,9 @@ Node EntailmentCheck::evaluateTerm2(TNode n, // must have the term if (reqHasTerm && !ret.isNull()) { - Kind k = ret.getKind(); - if (k != OR && k != AND && k != EQUAL && k != ITE && k != NOT - && k != FORALL) + Kind rk = ret.getKind(); + if (rk != OR && rk != AND && rk != EQUAL && rk != ITE && rk != NOT + && rk != FORALL) { if (!d_qstate.hasTerm(ret)) { @@ -215,19 +188,13 @@ Node EntailmentCheck::evaluateTerm2(TNode n, } Trace("term-db-eval") << "evaluated term : " << n << ", got : " << ret << ", reqHasTerm = " << reqHasTerm << std::endl; - // clear the explanation if failed - if (computeExp && ret.isNull()) - { - exp.resize(prevSize); - } visited[n] = ret; return ret; } TNode EntailmentCheck::getEntailedTerm2(TNode n, std::map& subs, - bool subsRep, - bool hasSubs) + bool subsRep) { Trace("term-db-entail") << "get entailed term : " << n << std::endl; if (d_qstate.hasTerm(n)) @@ -237,30 +204,27 @@ TNode EntailmentCheck::getEntailedTerm2(TNode n, } else if (n.getKind() == BOUND_VARIABLE) { - if (hasSubs) + std::map::iterator it = subs.find(n); + if (it != subs.end()) { - std::map::iterator it = subs.find(n); - if (it != subs.end()) + Trace("term-db-entail") + << "...substitution is : " << it->second << std::endl; + if (subsRep) { - Trace("term-db-entail") - << "...substitution is : " << it->second << std::endl; - if (subsRep) - { - Assert(d_qstate.hasTerm(it->second)); - Assert(d_qstate.getRepresentative(it->second) == it->second); - return it->second; - } - return getEntailedTerm2(it->second, subs, subsRep, hasSubs); + Assert(d_qstate.hasTerm(it->second)); + Assert(d_qstate.getRepresentative(it->second) == it->second); + return it->second; } + return getEntailedTerm2(it->second, subs, subsRep); } } else if (n.getKind() == ITE) { for (uint32_t i = 0; i < 2; i++) { - if (isEntailed2(n[0], subs, subsRep, hasSubs, i == 0)) + if (isEntailed2(n[0], subs, subsRep, i == 0)) { - return getEntailedTerm2(n[i == 0 ? 1 : 2], subs, subsRep, hasSubs); + return getEntailedTerm2(n[i == 0 ? 1 : 2], subs, subsRep); } } } @@ -274,7 +238,7 @@ TNode EntailmentCheck::getEntailedTerm2(TNode n, std::vector args; for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++) { - TNode c = getEntailedTerm2(n[i], subs, subsRep, hasSubs); + TNode c = getEntailedTerm2(n[i], subs, subsRep); if (c.isNull()) { return TNode::null(); @@ -294,48 +258,52 @@ TNode EntailmentCheck::getEntailedTerm2(TNode n, } Node EntailmentCheck::evaluateTerm(TNode n, + std::map& subs, + bool subsRep, bool useEntailmentTests, bool reqHasTerm) { std::map visited; - std::vector exp; - return evaluateTerm2(n, visited, exp, useEntailmentTests, false, reqHasTerm); + return evaluateTerm2( + n, visited, subs, subsRep, useEntailmentTests, reqHasTerm); } Node EntailmentCheck::evaluateTerm(TNode n, - std::vector& exp, bool useEntailmentTests, bool reqHasTerm) { std::map visited; - return evaluateTerm2(n, visited, exp, useEntailmentTests, true, reqHasTerm); + std::map subs; + return evaluateTerm2(n, visited, subs, false, useEntailmentTests, reqHasTerm); } TNode EntailmentCheck::getEntailedTerm(TNode n, std::map& subs, bool subsRep) { - return getEntailedTerm2(n, subs, subsRep, true); + return getEntailedTerm2(n, subs, subsRep); } TNode EntailmentCheck::getEntailedTerm(TNode n) { std::map subs; - return getEntailedTerm2(n, subs, false, false); + return getEntailedTerm2(n, subs, false); } -bool EntailmentCheck::isEntailed2( - TNode n, std::map& subs, bool subsRep, bool hasSubs, bool pol) +bool EntailmentCheck::isEntailed2(TNode n, + std::map& subs, + bool subsRep, + bool pol) { Trace("term-db-entail") << "Check entailed : " << n << ", pol = " << pol << std::endl; Assert(n.getType().isBoolean()); if (n.getKind() == EQUAL && !n[0].getType().isBoolean()) { - TNode n1 = getEntailedTerm2(n[0], subs, subsRep, hasSubs); + TNode n1 = getEntailedTerm2(n[0], subs, subsRep); if (!n1.isNull()) { - TNode n2 = getEntailedTerm2(n[1], subs, subsRep, hasSubs); + TNode n2 = getEntailedTerm2(n[1], subs, subsRep); if (!n2.isNull()) { if (n1 == n2) @@ -360,14 +328,14 @@ bool EntailmentCheck::isEntailed2( } else if (n.getKind() == NOT) { - return isEntailed2(n[0], subs, subsRep, hasSubs, !pol); + return isEntailed2(n[0], subs, subsRep, !pol); } else if (n.getKind() == OR || n.getKind() == AND) { bool simPol = (pol && n.getKind() == OR) || (!pol && n.getKind() == AND); for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++) { - if (isEntailed2(n[i], subs, subsRep, hasSubs, pol)) + if (isEntailed2(n[i], subs, subsRep, pol)) { if (simPol) { @@ -389,17 +357,17 @@ bool EntailmentCheck::isEntailed2( { for (size_t i = 0; i < 2; i++) { - if (isEntailed2(n[0], subs, subsRep, hasSubs, i == 0)) + if (isEntailed2(n[0], subs, subsRep, i == 0)) { size_t ch = (n.getKind() == EQUAL || i == 0) ? 1 : 2; bool reqPol = (n.getKind() == ITE || i == 0) ? pol : !pol; - return isEntailed2(n[ch], subs, subsRep, hasSubs, reqPol); + return isEntailed2(n[ch], subs, subsRep, reqPol); } } } else if (n.getKind() == APPLY_UF) { - TNode n1 = getEntailedTerm2(n, subs, subsRep, hasSubs); + TNode n1 = getEntailedTerm2(n, subs, subsRep); if (!n1.isNull()) { Assert(d_qstate.hasTerm(n1)); @@ -419,7 +387,7 @@ bool EntailmentCheck::isEntailed2( } else if (n.getKind() == FORALL && !pol) { - return isEntailed2(n[1], subs, subsRep, hasSubs, pol); + return isEntailed2(n[1], subs, subsRep, pol); } return false; } @@ -427,7 +395,7 @@ bool EntailmentCheck::isEntailed2( bool EntailmentCheck::isEntailed(TNode n, bool pol) { std::map subs; - return isEntailed2(n, subs, false, false, pol); + return isEntailed2(n, subs, false, pol); } bool EntailmentCheck::isEntailed(TNode n, @@ -435,7 +403,7 @@ bool EntailmentCheck::isEntailed(TNode n, bool subsRep, bool pol) { - return isEntailed2(n, subs, subsRep, true, pol); + return isEntailed2(n, subs, subsRep, pol); } } // namespace quantifiers diff --git a/src/theory/quantifiers/entailment_check.h b/src/theory/quantifiers/entailment_check.h index 5f0af60a6..ecf74fe85 100644 --- a/src/theory/quantifiers/entailment_check.h +++ b/src/theory/quantifiers/entailment_check.h @@ -44,19 +44,18 @@ class EntailmentCheck : protected EnvObj ~EntailmentCheck(); /** evaluate term * - * Returns a term n' such that n = n' is entailed based on the equality - * information ee. This function may generate new terms. In particular, - * we typically rewrite subterms of n of maximal size to terms that exist in - * the equality engine specified by ee. + * Returns a term n' such that n * subs = n' is entailed based on the current + * set of equalities, where ( n * subs ) is term n under the substitution + * subs. + * + * This function may generate new terms. In particular, we typically rewrite + * subterms of n of maximal size (in terms of the AST) to terms that exist + * in the equality engine. * * useEntailmentTests is whether to call the theory engine's entailmentTest * on literals n for which this call fails to find a term n' that is * equivalent to n, for increased precision. This is not frequently used. * - * The vector exp stores the explanation for why n evaluates to that term, - * that is, if this call returns a non-null node n', then: - * exp => n = n' - * * If reqHasTerm, then we require that the returned term is a Boolean * combination of terms that exist in the equality engine used by this call. * If no such term is constructable, this call returns null. The motivation @@ -64,12 +63,23 @@ class EntailmentCheck : protected EnvObj * of this function to only involve existing terms. This is used e.g. in * the "propagating instances" portion of conflict-based instantiation * (quant_conflict_find.h). + * + * @param n The term under consideration + * @param subs The substitution under consideration + * @param subsRep Whether the range of subs are representatives in the current + * equality engine + * @param useEntailmentTests Whether to use entailment tests to show + * n * subs is equivalent to true/false. + * @param reqHasTerm Whether we require the returned term to be a Boolean + * combination of terms known to the current equality engine + * @return the term n * subs evaluates to */ Node evaluateTerm(TNode n, - std::vector& exp, + std::map& subs, + bool subsRep, bool useEntailmentTests = false, bool reqHasTerm = false); - /** same as above, without exp */ + /** Same as above, without a substitution */ Node evaluateTerm(TNode n, bool useEntailmentTests = false, bool reqHasTerm = false); @@ -119,20 +129,16 @@ class EntailmentCheck : protected EnvObj /** helper for evaluate term */ Node evaluateTerm2(TNode n, std::map& visited, - std::vector& exp, + std::map& subs, + bool subsRep, bool useEntailmentTests, - bool computeExp, bool reqHasTerm); /** helper for get entailed term */ - TNode getEntailedTerm2(TNode n, - std::map& subs, - bool subsRep, - bool hasSubs); + TNode getEntailedTerm2(TNode n, std::map& subs, bool subsRep); /** helper for is entailed */ bool isEntailed2(TNode n, std::map& subs, bool subsRep, - bool hasSubs, bool pol); /** The quantifiers state object */ QuantifiersState& d_qstate; diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index dc1043d28..323398879 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -52,12 +52,6 @@ QuantInfo::~QuantInfo() { d_var_mg.clear(); } -QuantifiersInferenceManager& QuantInfo::getInferenceManager() -{ - Assert(d_parent != nullptr); - return d_parent->getInferenceManager(); -} - void QuantInfo::initialize( QuantConflictFind * p, Node q, Node qn ) { d_parent = p; d_q = q; @@ -578,29 +572,32 @@ bool QuantInfo::isTConstraintSpurious(QuantConflictFind* p, if( options::qcfEagerTest() ){ //check whether the instantiation evaluates as expected EntailmentCheck* echeck = p->getTermRegistry().getEntailmentCheck(); + std::map subs; + for (size_t i = 0, tsize = terms.size(); i < tsize; i++) + { + Trace("qcf-instance-check") << " " << terms[i] << std::endl; + subs[d_q[0][i]] = terms[i]; + } + for (size_t i = 0, evsize = d_extra_var.size(); i < evsize; i++) + { + Node n = getCurrentExpValue(d_extra_var[i]); + Trace("qcf-instance-check") + << " " << d_extra_var[i] << " -> " << n << std::endl; + subs[d_extra_var[i]] = n; + } if (p->atConflictEffort()) { Trace("qcf-instance-check") << "Possible conflict instance for " << d_q << " : " << std::endl; - std::map< TNode, TNode > subs; - for( unsigned i=0; i " << n << std::endl; - subs[d_extra_var[i]] = n; - } if (!echeck->isEntailed(d_q[1], subs, false, false)) { Trace("qcf-instance-check") << "...not entailed to be false." << std::endl; return true; } }else{ - Node inst = - getInferenceManager().getInstantiate()->getInstantiation(d_q, terms); - inst = Rewriter::rewrite(inst); - Node inst_eval = - echeck->evaluateTerm(inst, options::qcfTConstraint(), true); + // see if the body of the quantified formula evaluates to a Boolean + // combination of known terms under the current substitution. We use + // the helper method evaluateTerm from the entailment check utility. + Node inst_eval = echeck->evaluateTerm( + d_q[1], subs, false, options::qcfTConstraint(), true); if( Trace.isOn("qcf-instance-check") ){ Trace("qcf-instance-check") << "Possible propagating instance for " << d_q << " : " << std::endl; for( unsigned i=0; i())) { diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 927a74ff2..d14e281fb 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -132,8 +132,6 @@ public: public: QuantInfo(); ~QuantInfo(); - /** Get quantifiers inference manager */ - QuantifiersInferenceManager& getInferenceManager(); std::vector< TNode > d_vars; std::vector< TypeNode > d_var_types; std::map< TNode, int > d_var_num; -- cgit v1.2.3 From 628a13f0e5f95fb3372c0676e91a9e719fa05b8c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 20 Oct 2021 15:47:06 -0500 Subject: Make SyGuS solver robust to non-closed enumerable sorts (#7417) This makes the SyGuS solver robust to variables that are not closed enumerable, e.g. arrays of uninterpreted sorts. It corrects an issue in array's mkGroundTerm issue which would allow constants to enter into constraints for SyGuS problems with arrays. This method does not cause further issues currently since quantifiers is guarded in several places to ensure array constants are not constructed via this method. It also makes it so that we don't add explicit CEGIS refinement lemmas unless evaluation unfolding is enabled and the counterexamples are from closed enumerable types; there is no reason to add these unless we are combining with evaluation unfolding. This addresses several of the issues raised in #6605. --- src/theory/arrays/theory_arrays_type_rules.cpp | 20 +++++++++++++++- src/theory/quantifiers/sygus/cegis.cpp | 28 +++++++++++++++------- src/theory/quantifiers/sygus/cegis.h | 7 ++++++ .../quantifiers/sygus/sygus_grammar_cons.cpp | 3 +++ test/regress/CMakeLists.txt | 1 + test/regress/regress1/sygus/array-uc.sy | 14 +++++++++++ 6 files changed, 64 insertions(+), 9 deletions(-) create mode 100644 test/regress/regress1/sygus/array-uc.sy (limited to 'src') diff --git a/src/theory/arrays/theory_arrays_type_rules.cpp b/src/theory/arrays/theory_arrays_type_rules.cpp index e1b4813ec..433768e5d 100644 --- a/src/theory/arrays/theory_arrays_type_rules.cpp +++ b/src/theory/arrays/theory_arrays_type_rules.cpp @@ -18,6 +18,7 @@ // for array-constant attributes #include "expr/array_store_all.h" #include "theory/arrays/theory_arrays_rewriter.h" +#include "theory/builtin/theory_builtin_type_rules.h" #include "theory/type_enumerator.h" #include "util/cardinality.h" @@ -249,7 +250,24 @@ bool ArraysProperties::isWellFounded(TypeNode type) Node ArraysProperties::mkGroundTerm(TypeNode type) { - return *TypeEnumerator(type); + Assert(type.getKind() == kind::ARRAY_TYPE); + TypeNode elemType = type.getArrayConstituentType(); + Node elem = elemType.mkGroundTerm(); + if (elem.isConst()) + { + return NodeManager::currentNM()->mkConst(ArrayStoreAll(type, elem)); + } + // Note the distinction between mkGroundTerm and mkGroundValue. While + // an arbitrary value can be obtained by calling the type enumerator here, + // that is wrong for types that are not closed enumerable since it may + // return a term containing values that should not appear in e.g. assertions. + // For example, arrays whose element type is an uninterpreted sort will + // incorrectly introduce uninterpreted sort values if this is done. + // It is currently infeasible to construct an ArrayStoreAll with the element + // type's mkGroundTerm as an argument when that term is not constant. + // Thus, we must simply return a fresh Skolem here, using the same utility + // as that of uninterpreted sorts. + return builtin::SortProperties::mkGroundTerm(type); } TypeNode ArrayPartialSelectTypeRule::computeType(NodeManager* nodeManager, diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index c8e14e4bd..fdc0b28e0 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -39,6 +39,7 @@ Cegis::Cegis(Env& env, SynthConjecture* p) : SygusModule(env, qs, qim, tds, p), d_eval_unfold(tds->getEvalUnfold()), + d_cexClosedEnum(false), d_cegis_sampler(env), d_usingSymCons(false) { @@ -47,11 +48,18 @@ Cegis::Cegis(Env& env, bool Cegis::initialize(Node conj, Node n, const std::vector& candidates) { d_base_body = n; + d_cexClosedEnum = true; if (d_base_body.getKind() == NOT && d_base_body[0].getKind() == FORALL) { for (const Node& v : d_base_body[0][0]) { d_base_vars.push_back(v); + if (!v.getType().isClosedEnumerable()) + { + // not closed enumerable, refinement lemmas cannot be sent to the + // quantifier-free datatype solver + d_cexClosedEnum = false; + } } d_base_body = d_base_body[0][1]; } @@ -467,14 +475,18 @@ void Cegis::addRefinementLemmaConjunct(unsigned wcounter, void Cegis::registerRefinementLemma(const std::vector& vars, Node lem) { addRefinementLemma(lem); - // Make the refinement lemma and add it to lems. - // This lemma is guarded by the parent's guard, which has the semantics - // "this conjecture has a solution", hence this lemma states: - // if the parent conjecture has a solution, it satisfies the specification - // for the given concrete point. - Node rlem = - NodeManager::currentNM()->mkNode(OR, d_parent->getGuard().negate(), lem); - d_qim.addPendingLemma(rlem, InferenceId::QUANTIFIERS_SYGUS_CEGIS_REFINE); + // must be closed enumerable + if (d_cexClosedEnum && options().quantifiers.sygusEvalUnfold) + { + // Make the refinement lemma and add it to lems. + // This lemma is guarded by the parent's guard, which has the semantics + // "this conjecture has a solution", hence this lemma states: + // if the parent conjecture has a solution, it satisfies the specification + // for the given concrete point. + Node rlem = NodeManager::currentNM()->mkNode( + OR, d_parent->getGuard().negate(), lem); + d_qim.addPendingLemma(rlem, InferenceId::QUANTIFIERS_SYGUS_CEGIS_REFINE); + } } bool Cegis::usingRepairConst() { return true; } diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h index 8e0fffdd1..8d1f0a1b2 100644 --- a/src/theory/quantifiers/sygus/cegis.h +++ b/src/theory/quantifiers/sygus/cegis.h @@ -119,6 +119,13 @@ class Cegis : public SygusModule std::vector d_rl_vals; /** all variables appearing in refinement lemmas */ std::unordered_set d_refinement_lemma_vars; + /** + * Are the counterexamples we are handling in this class of only closed + * enumerable types (see TypeNode::isClosedEnumerable). If this is false, + * then CEGIS refinement lemmas can contain terms that are unhandled by + * theory solvers, e.g. uninterpreted constants. + */ + bool d_cexClosedEnum; /** adds lem as a refinement lemma */ void addRefinementLemma(Node lem); diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 43c958ff9..9b4cfb9e1 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -20,6 +20,7 @@ #include "expr/ascription_type.h" #include "expr/dtype_cons.h" +#include "expr/node_algorithm.h" #include "options/quantifiers_options.h" #include "theory/bv/theory_bv_utils.h" #include "theory/datatypes/sygus_datatype_utils.h" @@ -420,6 +421,8 @@ void CegGrammarConstructor::mkSygusConstantsForType(TypeNode type, { // generate constant array over the first element of the constituent type Node c = type.mkGroundTerm(); + // note that c should never contain an uninterpreted constant + Assert(!expr::hasSubtermKind(UNINTERPRETED_CONSTANT, c)); ops.push_back(c); } else if (type.isRoundingMode()) diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 6dafe6852..0f7b19e47 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2314,6 +2314,7 @@ set(regress_1_tests regress1/sygus/abv.sy regress1/sygus/array-grammar-store.sy regress1/sygus/array_search_5-Q-easy.sy + regress1/sygus/array-uc.sy regress1/sygus/bvudiv-by-2.sy regress1/sygus/cegar1.sy regress1/sygus/cegis-unif-inv-eq-fair.sy diff --git a/test/regress/regress1/sygus/array-uc.sy b/test/regress/regress1/sygus/array-uc.sy new file mode 100644 index 000000000..b3d950436 --- /dev/null +++ b/test/regress/regress1/sygus/array-uc.sy @@ -0,0 +1,14 @@ +; COMMAND-LINE: --sygus-out=status +; EXPECT: unsat +(set-logic ALL) +(declare-sort U 0) +(synth-fun f ((x (Array U Int)) (y U)) Bool) + +(declare-var x (Array U Int)) +(declare-var y U) + +(constraint (= (f (store x y 0) y) true)) +(constraint (= (f (store x y 1) y) false)) + +; f can be (= (select x y) 0) +(check-synth) -- cgit v1.2.3 From 09c6f9514b993c78c662ff6d3f46acce97286068 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 20 Oct 2021 16:07:09 -0500 Subject: Eliminate last static calls to rewriter from smt layer (#7355) --- src/proof/proof_node_manager.cpp | 7 ++++--- src/proof/proof_node_manager.h | 8 +++++++- src/smt/check_models.cpp | 5 ++--- src/smt/check_models.h | 10 ++-------- src/smt/model_blocker.cpp | 2 ++ src/smt/model_blocker.h | 6 ++++-- src/smt/preprocessor.cpp | 2 +- src/smt/proof_manager.cpp | 2 +- src/smt/proof_post_processor.cpp | 2 +- src/smt/solver_engine.cpp | 8 +++++--- src/smt/sygus_solver.cpp | 2 +- src/smt/witness_form.cpp | 18 ++++++++++++------ src/smt/witness_form.h | 11 ++++++++++- 13 files changed, 52 insertions(+), 31 deletions(-) (limited to 'src') diff --git a/src/proof/proof_node_manager.cpp b/src/proof/proof_node_manager.cpp index a3ef944e0..8b4b332a1 100644 --- a/src/proof/proof_node_manager.cpp +++ b/src/proof/proof_node_manager.cpp @@ -28,7 +28,8 @@ using namespace cvc5::kind; namespace cvc5 { -ProofNodeManager::ProofNodeManager(ProofChecker* pc) : d_checker(pc) +ProofNodeManager::ProofNodeManager(theory::Rewriter* rr, ProofChecker* pc) + : d_rewriter(rr), d_checker(pc) { d_true = NodeManager::currentNM()->mkConst(true); // we always allocate a proof checker, regardless of the proof checking mode @@ -160,14 +161,14 @@ std::shared_ptr ProofNodeManager::mkScope( computedAcr = true; for (const Node& acc : ac) { - Node accr = theory::Rewriter::rewrite(acc); + Node accr = d_rewriter->rewrite(acc); if (accr != acc) { acr[accr] = acc; } } } - Node ar = theory::Rewriter::rewrite(a); + Node ar = d_rewriter->rewrite(a); std::unordered_map::iterator itr = acr.find(ar); if (itr != acr.end()) { diff --git a/src/proof/proof_node_manager.h b/src/proof/proof_node_manager.h index 928aabb76..533f6d173 100644 --- a/src/proof/proof_node_manager.h +++ b/src/proof/proof_node_manager.h @@ -28,6 +28,10 @@ namespace cvc5 { class ProofChecker; class ProofNode; +namespace theory { +class Rewriter; +} + /** * A manager for proof node objects. This is a trusted interface for creating * and updating ProofNode objects. @@ -54,7 +58,7 @@ class ProofNode; class ProofNodeManager { public: - ProofNodeManager(ProofChecker* pc = nullptr); + ProofNodeManager(theory::Rewriter* rr, ProofChecker* pc = nullptr); ~ProofNodeManager() {} /** * This constructs a ProofNode with the given arguments. The expected @@ -184,6 +188,8 @@ class ProofNodeManager static ProofNode* cancelDoubleSymm(ProofNode* pn); private: + /** The rewriter */ + theory::Rewriter* d_rewriter; /** The (optional) proof checker */ ProofChecker* d_checker; /** the true node */ diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp index f148d1018..36d107429 100644 --- a/src/smt/check_models.cpp +++ b/src/smt/check_models.cpp @@ -31,8 +31,7 @@ using namespace cvc5::theory; namespace cvc5 { namespace smt { -CheckModels::CheckModels(Env& e) : d_env(e) {} -CheckModels::~CheckModels() {} +CheckModels::CheckModels(Env& e) : EnvObj(e) {} void CheckModels::checkModel(TheoryModel* m, const context::CDList& al, @@ -71,7 +70,7 @@ void CheckModels::checkModel(TheoryModel* m, Notice() << "SolverEngine::checkModel(): -- substitutes to " << n << std::endl; - n = Rewriter::rewrite(n); + n = rewrite(n); Notice() << "SolverEngine::checkModel(): -- rewrites to " << n << std::endl; // We look up the value before simplifying. If n contains quantifiers, diff --git a/src/smt/check_models.h b/src/smt/check_models.h index d785b53d5..2b3447010 100644 --- a/src/smt/check_models.h +++ b/src/smt/check_models.h @@ -20,11 +20,10 @@ #include "context/cdlist.h" #include "expr/node.h" +#include "smt/env_obj.h" namespace cvc5 { -class Env; - namespace theory { class TheoryModel; } @@ -34,11 +33,10 @@ namespace smt { /** * This utility is responsible for checking the current model. */ -class CheckModels +class CheckModels : protected EnvObj { public: CheckModels(Env& e); - ~CheckModels(); /** * Check model m against the current set of input assertions al. * @@ -48,10 +46,6 @@ class CheckModels void checkModel(theory::TheoryModel* m, const context::CDList& al, bool hardFailure); - - private: - /** Reference to the environment */ - Env& d_env; }; } // namespace smt diff --git a/src/smt/model_blocker.cpp b/src/smt/model_blocker.cpp index cbc388331..e8c1ff07f 100644 --- a/src/smt/model_blocker.cpp +++ b/src/smt/model_blocker.cpp @@ -25,6 +25,8 @@ using namespace cvc5::kind; namespace cvc5 { +ModelBlocker::ModelBlocker(Env& e) : EnvObj(e) {} + Node ModelBlocker::getModelBlocker(const std::vector& assertions, theory::TheoryModel* m, options::BlockModelsMode mode, diff --git a/src/smt/model_blocker.h b/src/smt/model_blocker.h index 42219e220..5e41de6a3 100644 --- a/src/smt/model_blocker.h +++ b/src/smt/model_blocker.h @@ -22,6 +22,7 @@ #include "expr/node.h" #include "options/smt_options.h" +#include "smt/env_obj.h" namespace cvc5 { @@ -32,9 +33,10 @@ class TheoryModel; /** * A utility for blocking the current model. */ -class ModelBlocker +class ModelBlocker : protected EnvObj { public: + ModelBlocker(Env& e); /** get model blocker * * This returns a disjunction of literals ~L1 V ... V ~Ln with the following @@ -63,7 +65,7 @@ class ModelBlocker * our input. In other words, we do not return ~(x < 0) V ~(w < 0) since the * left disjunct is always false. */ - static Node getModelBlocker( + Node getModelBlocker( const std::vector& assertions, theory::TheoryModel* m, options::BlockModelsMode mode, diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp index 4b16b9391..3aed58b30 100644 --- a/src/smt/preprocessor.cpp +++ b/src/smt/preprocessor.cpp @@ -150,7 +150,7 @@ Node Preprocessor::simplify(const Node& node) d_env.getPrinter().toStreamCmdSimplify(d_env.getDumpOut(), node); } Node ret = expandDefinitions(node); - ret = theory::Rewriter::rewrite(ret); + ret = rewrite(ret); return ret; } diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index 2e08ab2df..4b4291075 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -41,7 +41,7 @@ PfManager::PfManager(Env& env) d_pchecker(new ProofChecker( options().proof.proofCheck == options::ProofCheckMode::EAGER, options().proof.proofPedantic)), - d_pnm(new ProofNodeManager(d_pchecker.get())), + d_pnm(new ProofNodeManager(env.getRewriter(), d_pchecker.get())), d_pppg(new PreprocessProofGenerator( d_pnm.get(), env.getUserContext(), "smt::PreprocessProofGenerator")), d_pfpp(nullptr), diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index a547c4362..04a36c1c0 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -42,7 +42,7 @@ ProofPostprocessCallback::ProofPostprocessCallback(Env& env, : d_env(env), d_pnm(env.getProofNodeManager()), d_pppg(pppg), - d_wfpm(env.getProofNodeManager()), + d_wfpm(env), d_updateScopedAssumptions(updateScopedAssumptions) { d_true = NodeManager::currentNM()->mkConst(true); diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index e928dcade..fc6ec3915 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -1081,7 +1081,7 @@ Node SolverEngine::getValue(const Node& ex) const // AJR : necessary? if (!n.getType().isFunction()) { - n = Rewriter::rewrite(n); + n = d_env->getRewriter()->rewrite(n); } Trace("smt") << "--- getting value of " << n << endl; @@ -1224,7 +1224,8 @@ Result SolverEngine::blockModel() // get expanded assertions std::vector eassertsProc = getExpandedAssertions(); - Node eblocker = ModelBlocker::getModelBlocker( + ModelBlocker mb(*d_env.get()); + Node eblocker = mb.getModelBlocker( eassertsProc, m, d_env->getOptions().smt.blockModelsMode); Trace("smt") << "Block formula: " << eblocker << std::endl; return assertFormula(eblocker); @@ -1247,7 +1248,8 @@ Result SolverEngine::blockModelValues(const std::vector& exprs) // get expanded assertions std::vector eassertsProc = getExpandedAssertions(); // we always do block model values mode here - Node eblocker = ModelBlocker::getModelBlocker( + ModelBlocker mb(*d_env.get()); + Node eblocker = mb.getModelBlocker( eassertsProc, m, options::BlockModelsMode::VALUES, exprs); return assertFormula(eblocker); } diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp index 2a1d4e6c6..5db9804c6 100644 --- a/src/smt/sygus_solver.cpp +++ b/src/smt/sygus_solver.cpp @@ -377,7 +377,7 @@ void SygusSolver::checkSynthSolution(Assertions& as) // problem are rewritten to true. If this is not the case, then the // assertions module of the subsolver will complain about assertions // with free variables. - Node ar = theory::Rewriter::rewrite(a); + Node ar = rewrite(a); solChecker->assertFormula(ar); } Result r = solChecker->checkSat(); diff --git a/src/smt/witness_form.cpp b/src/smt/witness_form.cpp index 8e998b9cf..16d297495 100644 --- a/src/smt/witness_form.cpp +++ b/src/smt/witness_form.cpp @@ -16,21 +16,27 @@ #include "smt/witness_form.h" #include "expr/skolem_manager.h" +#include "smt/env.h" #include "theory/rewriter.h" namespace cvc5 { namespace smt { -WitnessFormGenerator::WitnessFormGenerator(ProofNodeManager* pnm) - : d_tcpg(pnm, +WitnessFormGenerator::WitnessFormGenerator(Env& env) + : d_rewriter(env.getRewriter()), + d_tcpg(env.getProofNodeManager(), nullptr, TConvPolicy::FIXPOINT, TConvCachePolicy::NEVER, "WfGenerator::TConvProofGenerator", nullptr, true), - d_wintroPf(pnm, nullptr, nullptr, "WfGenerator::LazyCDProof"), - d_pskPf(pnm, nullptr, "WfGenerator::PurifySkolemProof") + d_wintroPf(env.getProofNodeManager(), + nullptr, + nullptr, + "WfGenerator::LazyCDProof"), + d_pskPf( + env.getProofNodeManager(), nullptr, "WfGenerator::PurifySkolemProof") { } @@ -114,12 +120,12 @@ Node WitnessFormGenerator::convertToWitnessForm(Node t) bool WitnessFormGenerator::requiresWitnessFormTransform(Node t, Node s) const { - return theory::Rewriter::rewrite(t) != theory::Rewriter::rewrite(s); + return d_rewriter->rewrite(t) != d_rewriter->rewrite(s); } bool WitnessFormGenerator::requiresWitnessFormIntro(Node t) const { - Node tr = theory::Rewriter::rewrite(t); + Node tr = d_rewriter->rewrite(t); return !tr.isConst() || !tr.getConst(); } diff --git a/src/smt/witness_form.h b/src/smt/witness_form.h index 8522d41f0..06d60c1ed 100644 --- a/src/smt/witness_form.h +++ b/src/smt/witness_form.h @@ -25,6 +25,13 @@ #include "proof/proof_generator.h" namespace cvc5 { + +class Env; + +namespace theory { +class Rewriter; +} + namespace smt { /** @@ -37,7 +44,7 @@ namespace smt { class WitnessFormGenerator : public ProofGenerator { public: - WitnessFormGenerator(ProofNodeManager* pnm); + WitnessFormGenerator(Env& env); ~WitnessFormGenerator() {} /** * Get proof for, which expects an equality of the form t = toWitness(t). @@ -85,6 +92,8 @@ class WitnessFormGenerator : public ProofGenerator * Return a proof generator that can prove the given axiom exists. */ ProofGenerator* convertExistsInternal(Node exists); + /** The rewriter we are using */ + theory::Rewriter* d_rewriter; /** The term conversion proof generator */ TConvProofGenerator d_tcpg; /** The nodes we have already added rewrite steps for in d_tcpg */ -- cgit v1.2.3 From 57f8d6c04430277abdb98916b8ac407930abd215 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 20 Oct 2021 17:01:01 -0500 Subject: Check for higher-order variables in TheoryUF::ppRewrite (#7408) Fixes #7000. That sequence of API calls now throws a logic exception. --- src/theory/uf/ho_extension.cpp | 15 +++++++++------ src/theory/uf/theory_uf.cpp | 2 +- test/unit/api/solver_black.cpp | 16 ++++++++++++++++ 3 files changed, 26 insertions(+), 7 deletions(-) (limited to 'src') diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp index 096a47c86..fd7cd467e 100644 --- a/src/theory/uf/ho_extension.cpp +++ b/src/theory/uf/ho_extension.cpp @@ -43,13 +43,16 @@ HoExtension::HoExtension(Env& env, Node HoExtension::ppRewrite(Node node) { // convert HO_APPLY to APPLY_UF if fully applied - if (node[0].getType().getNumChildren() == 2) + if (node.getKind() == HO_APPLY) { - Trace("uf-ho") << "uf-ho : expanding definition : " << node << std::endl; - Node ret = getApplyUfForHoApply(node); - Trace("uf-ho") << "uf-ho : ppRewrite : " << node << " to " << ret - << std::endl; - return ret; + if (node[0].getType().getNumChildren() == 2) + { + Trace("uf-ho") << "uf-ho : expanding definition : " << node << std::endl; + Node ret = getApplyUfForHoApply(node); + Trace("uf-ho") << "uf-ho : ppRewrite : " << node << " to " << ret + << std::endl; + return ret; + } } return node; } diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index cd974d3e4..ca7dc6a73 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -212,7 +212,7 @@ TrustNode TheoryUF::ppRewrite(TNode node, std::vector& lems) Trace("uf-exp-def") << "TheoryUF::ppRewrite: expanding definition : " << node << std::endl; Kind k = node.getKind(); - if (k == kind::HO_APPLY) + if (k == kind::HO_APPLY || (node.isVar() && node.getType().isFunction())) { if (!logicInfo().isHigherOrder()) { diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp index d5137393e..a294ad6ca 100644 --- a/test/unit/api/solver_black.cpp +++ b/test/unit/api/solver_black.cpp @@ -2544,5 +2544,21 @@ TEST_F(TestApiBlackSolver, Output) ASSERT_NE(cvc5::null_os.rdbuf(), d_solver.getOutput("inst").rdbuf()); } + +TEST_F(TestApiBlackSolver, issue7000) +{ + Sort s1 = d_solver.getIntegerSort(); + Sort s2 = d_solver.mkFunctionSort(s1, s1); + Sort s3 = d_solver.getRealSort(); + Term t4 = d_solver.mkPi(); + Term t7 = d_solver.mkConst(s3, "_x5"); + Term t37 = d_solver.mkConst(s2, "_x32"); + Term t59 = d_solver.mkConst(s2, "_x51"); + Term t72 = d_solver.mkTerm(EQUAL, t37, t59); + Term t74 = d_solver.mkTerm(GT, t4, t7); + // throws logic exception since logic is not higher order by default + ASSERT_THROW(d_solver.checkEntailed({t72, t74, t72, t72}), CVC5ApiException); +} + } // namespace test } // namespace cvc5 -- cgit v1.2.3 From 04c1d3b5c6af01c77a6c38e24847d4458a14ef3b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 20 Oct 2021 17:09:07 -0500 Subject: Throw exception if checking model with separation logic heap (#7422) Fixes #5515. It is currently not possible to check-model with separation logic. Checking models requires either additional bookkeeping (heap per formula position) or otherwise is expensive to check. This makes us give a recoverable exception. --- src/smt/check_models.cpp | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'src') diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp index 36d107429..5d16c12ce 100644 --- a/src/smt/check_models.cpp +++ b/src/smt/check_models.cpp @@ -49,6 +49,12 @@ void CheckModels::checkModel(TheoryModel* m, throw RecoverableModalException( "Cannot run check-model on a model with approximate values."); } + Node sepHeap, sepNeq; + if (m->getHeapModel(sepHeap, sepNeq)) + { + throw RecoverableModalException( + "Cannot run check-model on a model with a separation logic heap."); + } theory::SubstitutionMap& sm = d_env.getTopLevelSubstitutions().get(); Trace("check-model") << "checkModel: Check assertions..." << std::endl; -- cgit v1.2.3 From c7a319286027448d678327f3e950b2e6138a6abb Mon Sep 17 00:00:00 2001 From: yoni206 Date: Thu, 21 Oct 2021 01:18:33 +0300 Subject: Add `isNull` and `isUpdater` to `Sort` class of python API (#7423) This adds two missing functions to the python API, along with tests for them. It also adds a missing test for the cpp API. --- src/api/python/cvc5.pxd | 2 ++ src/api/python/cvc5.pxi | 6 ++++++ test/python/unit/api/test_sort.py | 11 +++++++++++ test/unit/api/sort_black.cpp | 8 ++++++++ 4 files changed, 27 insertions(+) (limited to 'src') diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index 08bcc956a..e458b635d 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -308,6 +308,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": bint operator>(const Sort&) except + bint operator<=(const Sort&) except + bint operator>=(const Sort&) except + + bint isNull() except + bint isBoolean() except + bint isInteger() except + bint isReal() except + @@ -321,6 +322,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": bint isConstructor() except + bint isSelector() except + bint isTester() except + + bint isUpdater() except + bint isFunction() except + bint isPredicate() except + bint isTuple() except + diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 6b6d391e6..2ce8efb08 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -2205,6 +2205,9 @@ cdef class Sort: def __hash__(self): return csorthash(self.csort) + def isNull(self): + return self.csort.isNull() + def isBoolean(self): return self.csort.isBoolean() @@ -2244,6 +2247,9 @@ cdef class Sort: def isTester(self): return self.csort.isTester() + def isUpdater(self): + return self.csort.isUpdater() + def isFunction(self): return self.csort.isFunction() diff --git a/test/python/unit/api/test_sort.py b/test/python/unit/api/test_sort.py index db8cbff25..98cf76d76 100644 --- a/test/python/unit/api/test_sort.py +++ b/test/python/unit/api/test_sort.py @@ -60,6 +60,11 @@ def test_operators_comparison(solver): solver.getIntegerSort() > Sort(solver) solver.getIntegerSort() >= Sort(solver) +def test_is_null(solver): + x = Sort(solver) + assert x.isNull() + x = solver.getBooleanSort() + assert not x.isNull() def test_is_boolean(solver): assert solver.getBooleanSort().isBoolean() @@ -140,6 +145,12 @@ def test_is_tester(solver): assert cons_sort.isTester() Sort(solver).isTester() +def test_is_updater(solver): + dt_sort = create_datatype_sort(solver) + dt = dt_sort.getDatatype() + updater_sort = dt[0][0].getUpdaterTerm().getSort() + assert updater_sort.isUpdater() + Sort(solver).isUpdater() def test_is_function(solver): fun_sort = solver.mkFunctionSort(solver.getRealSort(), diff --git a/test/unit/api/sort_black.cpp b/test/unit/api/sort_black.cpp index 1e9505ee1..d0c755cf7 100644 --- a/test/unit/api/sort_black.cpp +++ b/test/unit/api/sort_black.cpp @@ -61,6 +61,14 @@ TEST_F(TestApiBlackSort, operators_comparison) ASSERT_NO_THROW(d_solver.getIntegerSort() >= Sort()); } +TEST_F(TestApiBlackSort, isNull) +{ + Sort x; + ASSERT_TRUE(x.isNull()); + x = d_solver.getBooleanSort(); + ASSERT_FALSE(x.isNull()); +} + TEST_F(TestApiBlackSort, isBoolean) { ASSERT_TRUE(d_solver.getBooleanSort().isBoolean()); -- cgit v1.2.3 From fae60561339d795eb532970b2b3b0e685d44d6cd Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 20 Oct 2021 17:39:12 -0500 Subject: Move variadic trie utility to its own file (#7410) Work towards a new internal fuzzing technique. The new fuzzing technique leverages elements of the IJCAR 2020 paper on abduction, this moves https://github.com/cvc5/cvc5/blob/master/src/theory/quantifiers/sygus/cegis_core_connective.h#L44 to its own file. A followup PR will break this and further utility methods out of this file. --- src/expr/CMakeLists.txt | 2 ++ src/expr/variadic_trie.cpp | 55 ++++++++++++++++++++++++++++++++++++++++++++++ src/expr/variadic_trie.h | 54 +++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 111 insertions(+) create mode 100644 src/expr/variadic_trie.cpp create mode 100644 src/expr/variadic_trie.h (limited to 'src') diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index 467500868..45ce01edb 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -97,6 +97,8 @@ libcvc5_add_sources( sygus_datatype.h uninterpreted_constant.cpp uninterpreted_constant.h + variadic_trie.cpp + variadic_trie.h ) libcvc5_add_sources(GENERATED diff --git a/src/expr/variadic_trie.cpp b/src/expr/variadic_trie.cpp new file mode 100644 index 000000000..bd27780e9 --- /dev/null +++ b/src/expr/variadic_trie.cpp @@ -0,0 +1,55 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Variadic trie utility + */ + +#include "expr/variadic_trie.h" + +namespace cvc5 { + +bool VariadicTrie::add(Node n, const std::vector& i) +{ + VariadicTrie* curr = this; + for (const Node& ic : i) + { + curr = &(curr->d_children[ic]); + } + if (curr->d_data.isNull()) + { + curr->d_data = n; + return true; + } + return false; +} + +bool VariadicTrie::hasSubset(const std::vector& is) const +{ + if (!d_data.isNull()) + { + return true; + } + for (const std::pair& p : d_children) + { + Node n = p.first; + if (std::find(is.begin(), is.end(), n) != is.end()) + { + if (p.second.hasSubset(is)) + { + return true; + } + } + } + return false; +} + +} // namespace cvc5 diff --git a/src/expr/variadic_trie.h b/src/expr/variadic_trie.h new file mode 100644 index 000000000..aa7ca1e37 --- /dev/null +++ b/src/expr/variadic_trie.h @@ -0,0 +1,54 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Variadic trie utility + */ + +#include "cvc5_private.h" + +#ifndef CVC5__EXPR__VARIADIC_TRIE_H +#define CVC5__EXPR__VARIADIC_TRIE_H + +#include +#include + +#include "expr/node.h" + +namespace cvc5 { + +/** + * A trie that stores data at undetermined depth. Storing data at + * undetermined depth is in contrast to the NodeTrie (expr/node_trie.h), which + * assumes all data is stored at a fixed depth. + * + * Since data can be stored at any depth, we require both a d_children field + * and a d_data field. + */ +class VariadicTrie +{ + public: + /** the children of this node */ + std::map d_children; + /** the data at this node */ + Node d_data; + /** + * Add data with identifier n indexed by i, return true if data is not already + * stored at the node indexed by i. + */ + bool add(Node n, const std::vector& i); + /** Is there any data in this trie that is indexed by any subset of is? */ + bool hasSubset(const std::vector& is) const; +}; + +} // namespace cvc5 + +#endif /* CVC5__EXPR__VARIADIC_TRIE_H */ -- cgit v1.2.3 From 80cdf28298c9190506f37721492680f432ef635d Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 20 Oct 2021 15:56:40 -0700 Subject: api: Improve documentation for special cases with nullary ops. (#7433) Fixes #7430. --- src/api/cpp/cvc5.h | 13 +++++++++++++ src/api/cpp/cvc5_kind.h | 7 +++++++ src/theory/sets/normal_form.h | 2 +- 3 files changed, 21 insertions(+), 1 deletion(-) (limited to 'src') diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index ded477a9d..e6a19c771 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -1353,6 +1353,8 @@ class CVC5_EXPORT Term std::pair getReal64Value() const; /** * @return true if the term is a rational value. + * + * Note that a term of kind PI is not considered to be a real value. */ bool isRealValue() const; /** @@ -1448,6 +1450,17 @@ class CVC5_EXPORT Term /** * @return true if the term is a set value. + * + * A term is a set value if it is considered to be a (canonical) constant set + * value. A canonical set value is one whose AST is: + * ``` + * (union (singleton c1) ... (union (singleton c_{n-1}) (singleton c_n)))) + * ``` + * where `c1 ... cn` are values ordered by id such that `c1 > ... > cn` (see + * also @ref Term::operator>(const Term&) const). + * + * Note that a universe set term (kind UNIVERSE_SET) is not considered to be + * a set value. */ bool isSetValue() const; /** diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index 0ff05022f..fe87df934 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -766,6 +766,9 @@ enum CVC5_EXPORT Kind : int32_t /** * Pi constant. * + * Note that PI is considered a special symbol of sort Real, but is not + * a real value, i.e., `Term::isRealValue() const` will return false. + * * Create with: * - `Solver::mkPi() const` * - `Solver::mkTerm(Kind kind) const` @@ -2228,6 +2231,10 @@ enum CVC5_EXPORT Kind : int32_t * Finite universe set. * All set variables must be interpreted as subsets of it. * + * Note that UNIVERSE_SET is considered a special symbol of the theory of + * sets and is not considered as a set value, + * i.e., `Term::isSetValue() const` will return false. + * * Create with: * - `Solver::mkUniverseSet(const Sort& sort) const` */ diff --git a/src/theory/sets/normal_form.h b/src/theory/sets/normal_form.h index eb839e1c0..35d06a510 100644 --- a/src/theory/sets/normal_form.h +++ b/src/theory/sets/normal_form.h @@ -58,7 +58,7 @@ class NormalForm { } /** - * Returns true if n is considered a to be a (canonical) constant set value. + * Returns true if n is considered to be a (canonical) constant set value. * A canonical set value is one whose AST is: * (union (singleton c1) ... (union (singleton c_{n-1}) (singleton c_n)))) * where c1 ... cn are constants and the node identifier of these constants -- cgit v1.2.3 From bef33ceaf0a6b69d76b4fd61cb03c990e86bc41c Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 20 Oct 2021 16:12:55 -0700 Subject: api: Add Solver::mkSepEmp(). (#7432) @alex-ozdemir --- src/api/cpp/cvc5.cpp | 14 +++++++++++++- src/api/cpp/cvc5.h | 6 ++++++ src/api/java/cvc5/Solver.java | 12 ++++++++++++ src/api/java/jni/cvc5_Solver.cpp | 18 +++++++++++++++++- src/api/python/cvc5.pxd | 1 + src/api/python/cvc5.pxi | 9 +++++++++ src/parser/smt2/smt2.cpp | 16 +++++++--------- test/python/unit/api/test_solver.py | 4 ++++ test/unit/api/java/cvc5/SolverTest.java | 7 ++++++- test/unit/api/solver_black.cpp | 2 ++ 10 files changed, 77 insertions(+), 12 deletions(-) (limited to 'src') diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 2bc101bec..bb39ae86d 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -5082,7 +5082,7 @@ Term Solver::mkTermFromKind(Kind kind) const CVC5_API_KIND_CHECK_EXPECTED(kind == PI || kind == REGEXP_EMPTY || kind == REGEXP_SIGMA || kind == SEP_EMP, kind) - << "PI or REGEXP_EMPTY or REGEXP_SIGMA"; + << "PI, REGEXP_EMPTY, REGEXP_SIGMA or SEP_EMP"; //////// all checks before this line Node res; cvc5::Kind k = extToIntKind(kind); @@ -5822,6 +5822,18 @@ Term Solver::mkEmptyBag(const Sort& sort) const CVC5_API_TRY_CATCH_END; } +Term Solver::mkSepEmp() const +{ + CVC5_API_TRY_CATCH_BEGIN; + //////// all checks before this line + Node res = getNodeManager()->mkNullaryOperator(d_nodeMgr->booleanType(), + cvc5::Kind::SEP_EMP); + (void)res.getType(true); /* kick off type checking */ + return Term(this, res); + //////// + CVC5_API_TRY_CATCH_END; +} + Term Solver::mkSepNil(const Sort& sort) const { CVC5_API_TRY_CATCH_BEGIN; diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index e6a19c771..c46b00d0e 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -3443,6 +3443,12 @@ class CVC5_EXPORT Solver */ Term mkEmptyBag(const Sort& sort) const; + /** + * Create a separation logic empty term. + * @return the separation logic empty term + */ + Term mkSepEmp() const; + /** * Create a separation logic nil term. * @param sort the sort of the nil term diff --git a/src/api/java/cvc5/Solver.java b/src/api/java/cvc5/Solver.java index b0bee500c..c46d60aee 100644 --- a/src/api/java/cvc5/Solver.java +++ b/src/api/java/cvc5/Solver.java @@ -881,6 +881,18 @@ public class Solver implements IPointer private native long mkEmptyBag(long pointer, long sortPointer); + /** + * Create a separation logic empty term. + * @return the separation logic empty term + */ + public Term mkSepEmp() + { + long termPointer = mkSepEmp(pointer); + return new Term(this, termPointer); + } + + private native long mkSepEmp(long pointer); + /** * Create a separation logic nil term. * @param sort the sort of the nil term diff --git a/src/api/java/jni/cvc5_Solver.cpp b/src/api/java/jni/cvc5_Solver.cpp index c28ea412f..53c050c96 100644 --- a/src/api/java/jni/cvc5_Solver.cpp +++ b/src/api/java/jni/cvc5_Solver.cpp @@ -1059,6 +1059,22 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkEmptyBag(JNIEnv* env, CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } +/* + * Class: cvc5_Solver + * Method: mkSepEmp + * Signature: (JJ)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkSepEmp(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast(pointer); + Term* retPointer = new Term(solver->mkSepEmp()); + return reinterpret_cast(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + /* * Class: cvc5_Solver * Method: mkSepNil @@ -2591,4 +2607,4 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_getNullDatatypeDecl(JNIEnv* env, DatatypeDecl* ret = new DatatypeDecl(); return reinterpret_cast(ret); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); -} \ No newline at end of file +} diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index e458b635d..02b572120 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -219,6 +219,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": Term mkRegexpSigma() except + Term mkEmptySet(Sort s) except + Term mkEmptyBag(Sort s) except + + Term mkSepEmp() except + Term mkSepNil(Sort sort) except + Term mkString(const string& s) except + Term mkString(const wstring& s) except + diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 2ce8efb08..4627859b9 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -1168,6 +1168,15 @@ cdef class Solver: term.cterm = self.csolver.mkEmptyBag(s.csort) return term + def mkSepEmp(self): + """Create a separation logic empty term. + + :return: the separation logic empty term + """ + cdef Term term = Term(self) + term.cterm = self.csolver.mkSepEmp() + return term + def mkSepNil(self, Sort sort): """Create a separation logic nil term. diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index e1ce29b65..be7bdcb0f 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -263,14 +263,16 @@ void Smt2::addFloatingPointOperators() { } void Smt2::addSepOperators() { + defineVar("sep.emp", d_solver->mkSepEmp()); + // the Boolean sort is a placeholder here since we don't have type info + // without type annotation + defineVar("sep.nil", d_solver->mkSepNil(d_solver->getBooleanSort())); addOperator(api::SEP_STAR, "sep"); addOperator(api::SEP_PTO, "pto"); addOperator(api::SEP_WAND, "wand"); - addOperator(api::SEP_EMP, "emp"); Parser::addOperator(api::SEP_STAR); Parser::addOperator(api::SEP_PTO); Parser::addOperator(api::SEP_WAND); - Parser::addOperator(api::SEP_EMP); } void Smt2::addCoreSymbols() @@ -551,7 +553,7 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) if (d_logic.areTranscendentalsUsed()) { - defineVar("real.pi", d_solver->mkTerm(api::PI)); + defineVar("real.pi", d_solver->mkPi()); addTranscendentalOperators(); } if (!strictModeEnabled()) @@ -677,12 +679,8 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) addFloatingPointOperators(); } - if (d_logic.isTheoryEnabled(theory::THEORY_SEP)) { - // the Boolean sort is a placeholder here since we don't have type info - // without type annotation - defineVar("sep.nil", d_solver->mkSepNil(d_solver->getBooleanSort())); - defineVar("sep.emp", d_solver->mkTerm(api::SEP_EMP)); - + if (d_logic.isTheoryEnabled(theory::THEORY_SEP)) + { addSepOperators(); } diff --git a/test/python/unit/api/test_solver.py b/test/python/unit/api/test_solver.py index 29d637dc6..6052a057f 100644 --- a/test/python/unit/api/test_solver.py +++ b/test/python/unit/api/test_solver.py @@ -644,6 +644,10 @@ def test_mk_regexp_sigma(solver): solver.mkTerm(kinds.StringInRegexp, s, solver.mkRegexpSigma()) +def test_mk_sep_emp(solver): + solver.mkSepEmp(); + + def test_mk_sep_nil(solver): solver.mkSepNil(solver.getBooleanSort()) with pytest.raises(RuntimeError): diff --git a/test/unit/api/java/cvc5/SolverTest.java b/test/unit/api/java/cvc5/SolverTest.java index d153b8a91..6f9d8206d 100644 --- a/test/unit/api/java/cvc5/SolverTest.java +++ b/test/unit/api/java/cvc5/SolverTest.java @@ -623,6 +623,11 @@ class SolverTest assertDoesNotThrow(() -> d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpSigma())); } + @Test void mkSepEmp() + { + assertDoesNotThrow(() -> d_solver.mkSepEmp()); + } + @Test void mkSepNil() { assertDoesNotThrow(() -> d_solver.mkSepNil(d_solver.getBooleanSort())); @@ -2342,4 +2347,4 @@ class SolverTest + "\"Z\")))", projection.toString()); } -} \ No newline at end of file +} diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp index a294ad6ca..c9527c2d4 100644 --- a/test/unit/api/solver_black.cpp +++ b/test/unit/api/solver_black.cpp @@ -597,6 +597,8 @@ TEST_F(TestApiBlackSolver, mkRegexpSigma) d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpSigma())); } +TEST_F(TestApiBlackSolver, mkSepEmp) { ASSERT_NO_THROW(d_solver.mkSepEmp()); } + TEST_F(TestApiBlackSolver, mkSepNil) { ASSERT_NO_THROW(d_solver.mkSepNil(d_solver.getBooleanSort())); -- cgit v1.2.3 From e590612dc4421d45cacc451a7b8a162acd9c7943 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 20 Oct 2021 18:22:55 -0700 Subject: Fix (#7437) This PR reintroduces support for the (deprecated) option interactive-mode. It was erroneously removed in #7295. Fixes #7379. --- src/options/smt_options.toml | 1 + test/regress/CMakeLists.txt | 1 + test/regress/regress0/options/interactive-mode.smt2 | 10 ++++++++++ 3 files changed, 12 insertions(+) create mode 100644 test/regress/regress0/options/interactive-mode.smt2 (limited to 'src') diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 19862cab2..420496190 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -259,6 +259,7 @@ name = "SMT Layer" category = "common" long = "produce-assertions" type = "bool" + alias = ["interactive-mode"] help = "keep an assertions list (enables get-assertions command)" [[option]] diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 0d8123aa3..fca1543c4 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -767,6 +767,7 @@ set(regress_0_tests regress0/nl/very-simple-unsat.smt2 regress0/opt-abd-no-use.smt2 regress0/options/ast-and-sexpr.smt2 + regress0/options/interactive-mode.smt2 regress0/options/invalid_dump.smt2 regress0/options/set-after-init.smt2 regress0/options/set-and-get-options.smt2 diff --git a/test/regress/regress0/options/interactive-mode.smt2 b/test/regress/regress0/options/interactive-mode.smt2 new file mode 100644 index 000000000..549fdfd24 --- /dev/null +++ b/test/regress/regress0/options/interactive-mode.smt2 @@ -0,0 +1,10 @@ +; EXPECT: true +; EXPECT: true +; EXPECT: false +; EXPECT: false +(set-option :interactive-mode true) +(get-option :interactive-mode) +(get-option :produce-assertions) +(set-option :produce-assertions false) +(get-option :interactive-mode) +(get-option :produce-assertions) \ No newline at end of file -- cgit v1.2.3