From cc8ce1bcdf8d6a4b508723063879e891a6cbd8c3 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 20 Apr 2021 16:40:12 -0500 Subject: [PATCH] Add instantiation pool feature to the API (#6358) This adds the command declare-pool to the public API. It also adds parsing support for this feature, lifts the internal kinds to public kinds, adds an example regression, and a unit test for the new declare-pool solver method. --- src/CMakeLists.txt | 2 + src/api/cpp/cvc5.cpp | 24 +++++++++ src/api/cpp/cvc5.h | 13 +++++ src/api/cpp/cvc5_kind.h | 28 ++++++++++ src/api/python/cvc4.pxd | 1 + src/api/python/cvc4.pxi | 8 +++ src/parser/smt2/Smt2.g | 47 +++++++++------- src/printer/printer.cpp | 8 +++ src/printer/printer.h | 5 ++ src/smt/command.cpp | 54 +++++++++++++++++++ src/smt/command.h | 26 +++++++++ test/regress/CMakeLists.txt | 1 + .../regress1/quantifiers/pool-example.smt2 | 17 ++++++ test/unit/api/solver_black.cpp | 16 ++++++ 14 files changed, 232 insertions(+), 18 deletions(-) create mode 100644 test/regress/regress1/quantifiers/pool-example.smt2 diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index b86435eb7..c24ab31ec 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -869,6 +869,8 @@ libcvc4_add_sources( theory/quantifiers/term_database.h theory/quantifiers/term_enumeration.cpp theory/quantifiers/term_enumeration.h + theory/quantifiers/term_pools.cpp + theory/quantifiers/term_pools.h theory/quantifiers/term_registry.cpp theory/quantifiers/term_registry.h theory/quantifiers/term_util.cpp diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index a32ff4caa..aafc5331a 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -350,6 +350,9 @@ const static std::unordered_map s_kinds{ {BOUND_VAR_LIST, cvc5::Kind::BOUND_VAR_LIST}, {INST_PATTERN, cvc5::Kind::INST_PATTERN}, {INST_NO_PATTERN, cvc5::Kind::INST_NO_PATTERN}, + {INST_POOL, cvc5::Kind::INST_POOL}, + {INST_ADD_TO_POOL, cvc5::Kind::INST_ADD_TO_POOL}, + {SKOLEM_ADD_TO_POOL, cvc5::Kind::SKOLEM_ADD_TO_POOL}, {INST_ATTRIBUTE, cvc5::Kind::INST_ATTRIBUTE}, {INST_PATTERN_LIST, cvc5::Kind::INST_PATTERN_LIST}, {LAST_KIND, cvc5::Kind::LAST_KIND}, @@ -644,6 +647,9 @@ const static std::unordered_map {cvc5::Kind::BOUND_VAR_LIST, BOUND_VAR_LIST}, {cvc5::Kind::INST_PATTERN, INST_PATTERN}, {cvc5::Kind::INST_NO_PATTERN, INST_NO_PATTERN}, + {cvc5::Kind::INST_POOL, INST_POOL}, + {cvc5::Kind::INST_ADD_TO_POOL, INST_ADD_TO_POOL}, + {cvc5::Kind::SKOLEM_ADD_TO_POOL, SKOLEM_ADD_TO_POOL}, {cvc5::Kind::INST_ATTRIBUTE, INST_ATTRIBUTE}, {cvc5::Kind::INST_PATTERN_LIST, INST_PATTERN_LIST}, /* ----------------------------------------------------------------- */ @@ -6596,6 +6602,24 @@ Term Solver::getSeparationNilTerm() const CVC5_API_TRY_CATCH_END; } +Term Solver::declarePool(const std::string& symbol, + const Sort& sort, + const std::vector& initValue) const +{ + NodeManagerScope scope(getNodeManager()); + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_SOLVER_CHECK_SORT(sort); + CVC5_API_SOLVER_CHECK_TERMS(initValue); + //////// all checks before this line + TypeNode setType = getNodeManager()->mkSetType(*sort.d_type); + Node pool = getNodeManager()->mkBoundVar(symbol, setType); + std::vector initv = Term::termVectorToNodes(initValue); + d_smtEngine->declarePool(pool, initv); + return Term(this, pool); + //////// + CVC5_API_TRY_CATCH_END; +} + void Solver::pop(uint32_t nscopes) const { NodeManagerScope scope(getNodeManager()); diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index dc834d8b5..aaf19c30b 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -3566,6 +3566,19 @@ class CVC4_EXPORT Solver */ Term getSeparationNilTerm() const; + /** + * Declare a symbolic pool of terms with the given initial value. + * SMT-LIB: + * \verbatim + * ( declare-pool ( * ) ) + * \endverbatim + * @param symbol The name of the pool + * @param sort The sort of the elements of the pool. + * @param initValue The initial value of the pool + */ + Term declarePool(const std::string& symbol, + const Sort& sort, + const std::vector& initValue) const; /** * Pop (a) level(s) from the assertion stack. * SMT-LIB: diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index 6cb4be3c8..86e6d676d 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -3331,6 +3331,34 @@ enum CVC4_EXPORT Kind : int32_t * - `Solver::mkTerm(Kind kind, const std::vector& children) const` */ INST_NO_PATTERN, + /* + * An instantiation pool. + * Specifies an annotation for pool based instantiation. + * Parameters: n > 1 + * - 1..n: Terms that comprise the pools, which are one-to-one with + * the variables of the quantified formula to be instantiated. + * Create with: + * - `mkTerm(Kind kind, Term child1, Term child2) + * - `mkTerm(Kind kind, Term child1, Term child2, Term child3) + * - `mkTerm(Kind kind, const std::vector& children) + */ + INST_POOL, + /* + * A instantantiation-add-to-pool annotation. + * Parameters: n = 1 + * - 1: The pool to add to. + * Create with: + * - `mkTerm(Kind kind, Term child) + */ + INST_ADD_TO_POOL, + /* + * A skolemization-add-to-pool annotation. + * Parameters: n = 1 + * - 1: The pool to add to. + * Create with: + * - `mkTerm(Kind kind, Term child) + */ + SKOLEM_ADD_TO_POOL, /** * An instantiation attribute * Specifies a custom property for a quantified formula given by a diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd index abc23ea4b..336def3dc 100644 --- a/src/api/python/cvc4.pxd +++ b/src/api/python/cvc4.pxd @@ -240,6 +240,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": void declareSeparationHeap(Sort locSort, Sort dataSort) except + Term getSeparationHeap() except + Term getSeparationNilTerm() except + + Term declarePool(const string& name, Sort sort, vector[Term]& initValue) except + void pop(uint32_t nscopes) except + void push(uint32_t nscopes) except + void reset() except + diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi index 3156b0882..48921dc87 100644 --- a/src/api/python/cvc4.pxi +++ b/src/api/python/cvc4.pxi @@ -1136,6 +1136,14 @@ cdef class Solver: term.cterm = self.csolver.getSeparationNilTerm() return term + def declarePool(self, str symbol, Sort sort, initValue): + cdef Term term = Term(self) + cdef vector[c_Term] niv + for v in initValue: + niv.push_back(( v).cterm) + term.cterm = self.csolver.declarePool(symbol.encode(), sort.csort, niv) + return term + def pop(self, nscopes=1): self.csolver.pop(nscopes) diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index c347dc0db..4a612ce6f 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1059,6 +1059,19 @@ extendedCommand[std::unique_ptr* cmd] sortSymbol[s, CHECK_DECLARED] { cmd->reset(new DeclareHeapCommand(t, s)); } RPAREN_TOK + | DECLARE_POOL { PARSER_STATE->checkThatLogicIsSet(); } + symbol[name,CHECK_NONE,SYM_VARIABLE] + { PARSER_STATE->checkUserSymbol(name); } + sortSymbol[t,CHECK_DECLARED] + LPAREN_TOK + ( term[e, e2] + { terms.push_back( e ); } + )* RPAREN_TOK + { Debug("parser") << "declare pool: '" << name << "'" << std::endl; + api::Term pool = SOLVER->declarePool(name, t, terms); + PARSER_STATE->defineVar(name, pool); + cmd->reset(new DeclarePoolCommand(name, pool, t, terms)); + } | BLOCK_MODEL_TOK { PARSER_STATE->checkThatLogicIsSet(); } { cmd->reset(new BlockModelCommand()); } @@ -1468,7 +1481,7 @@ termNonVariable[cvc5::api::Term& expr, cvc5::api::Term& expr2] /* attributed expressions */ | LPAREN_TOK ATTRIBUTE_TOK term[expr, f2] - ( attribute[expr, attexpr, attr] + ( attribute[expr, attexpr] { if( ! attexpr.isNull()) { patexprs.push_back( attexpr ); } @@ -1478,14 +1491,7 @@ termNonVariable[cvc5::api::Term& expr, cvc5::api::Term& expr2] if(! patexprs.empty()) { if( !f2.isNull() && f2.getKind()==api::INST_PATTERN_LIST ){ for( size_t i=0; iwarning(ss.str()); - } + patexprs.push_back( f2[i] ); } } expr2 = MK_TERM(api::INST_PATTERN_LIST, patexprs); @@ -1745,7 +1751,7 @@ termAtomic[cvc5::api::Term& atomTerm] /** * Read attribute */ -attribute[cvc5::api::Term& expr, cvc5::api::Term& retExpr, std::string& attr] +attribute[cvc5::api::Term& expr, cvc5::api::Term& retExpr] @init { api::Term sexpr; std::string s; @@ -1753,23 +1759,26 @@ attribute[cvc5::api::Term& expr, cvc5::api::Term& retExpr, std::string& attr] std::vector patexprs; cvc5::api::Term e2; bool hasValue = false; + api::Kind k; } : KEYWORD ( simpleSymbolicExprNoKeyword[s] { hasValue = true; } )? { - attr = AntlrInput::tokenText($KEYWORD); - PARSER_STATE->attributeNotSupported(attr); + PARSER_STATE->attributeNotSupported(AntlrInput::tokenText($KEYWORD)); } - | ATTRIBUTE_PATTERN_TOK LPAREN_TOK + | ( ATTRIBUTE_PATTERN_TOK { k = api::INST_PATTERN; } | + ATTRIBUTE_POOL_TOK { k = api::INST_POOL; } | + ATTRIBUTE_INST_ADD_TO_POOL_TOK { k = api::INST_ADD_TO_POOL; } | + ATTRIBUTE_SKOLEM_ADD_TO_POOL_TOK{ k = api::SKOLEM_ADD_TO_POOL; } + ) + LPAREN_TOK ( term[patexpr, e2] { patexprs.push_back( patexpr ); } )+ RPAREN_TOK { - attr = std::string(":pattern"); - retExpr = MK_TERM(api::INST_PATTERN, patexprs); + retExpr = MK_TERM(k, patexprs); } | ATTRIBUTE_NO_PATTERN_TOK term[patexpr, e2] { - attr = std::string(":no-pattern"); retExpr = MK_TERM(api::INST_NO_PATTERN, patexpr); } | tok=( ATTRIBUTE_INST_LEVEL ) INTEGER_LITERAL @@ -1792,7 +1801,6 @@ attribute[cvc5::api::Term& expr, cvc5::api::Term& retExpr, std::string& attr] { api::Sort boolType = SOLVER->getBooleanSort(); api::Term avar = SOLVER->mkConst(boolType, sexprToString(sexpr)); - attr = std::string(":qid"); retExpr = MK_TERM(api::INST_ATTRIBUTE, avar); Command* c = new SetUserAttributeCommand("qid", avar); c->setMuted(true); @@ -1800,7 +1808,6 @@ attribute[cvc5::api::Term& expr, cvc5::api::Term& retExpr, std::string& attr] } | ATTRIBUTE_NAMED_TOK symbolicExpr[sexpr] { - attr = std::string(":named"); // notify that expression was given a name PARSER_STATE->notifyNamedExpression(expr, sexprToString(sexpr)); } @@ -2237,6 +2244,7 @@ GET_QE_DISJUNCT_TOK : 'get-qe-disjunct'; GET_ABDUCT_TOK : 'get-abduct'; GET_INTERPOL_TOK : 'get-interpol'; DECLARE_HEAP : 'declare-heap'; +DECLARE_POOL : 'declare-pool'; // SyGuS commands SYNTH_FUN_TOK : { PARSER_STATE->sygus() }?'synth-fun'; @@ -2252,6 +2260,9 @@ SYGUS_VARIABLE_TOK : { PARSER_STATE->sygus() }? 'Variable'; // attributes ATTRIBUTE_PATTERN_TOK : ':pattern'; ATTRIBUTE_NO_PATTERN_TOK : ':no-pattern'; +ATTRIBUTE_POOL_TOK : ':pool'; +ATTRIBUTE_INST_ADD_TO_POOL_TOK : ':inst-add-to-pool'; +ATTRIBUTE_SKOLEM_ADD_TO_POOL_TOK : ':skolem-add-to-pool'; ATTRIBUTE_NAMED_TOK : ':named'; ATTRIBUTE_INST_LEVEL : ':quant-inst-max-level'; ATTRIBUTE_QUANTIFIER_ID_TOK : ':qid'; diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index 6ab419b85..19d14eb09 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -190,6 +190,14 @@ void Printer::toStreamCmdDeclareFunction(std::ostream& out, printUnknownCommand(out, "declare-fun"); } +void Printer::toStreamCmdDeclarePool(std::ostream& out, + const std::string& id, + TypeNode type, + const std::vector& initValue) const +{ + printUnknownCommand(out, "declare-pool"); +} + void Printer::toStreamCmdDeclareType(std::ostream& out, TypeNode type) const { diff --git a/src/printer/printer.h b/src/printer/printer.h index aeffc76eb..86f3dbb2b 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -87,6 +87,11 @@ class Printer virtual void toStreamCmdDeclareFunction(std::ostream& out, const std::string& id, TypeNode type) const; + /** Print declare-pool command */ + virtual void toStreamCmdDeclarePool(std::ostream& out, + const std::string& id, + TypeNode type, + const std::vector& initValue) const; /** Print declare-sort command */ virtual void toStreamCmdDeclareType(std::ostream& out, diff --git a/src/smt/command.cpp b/src/smt/command.cpp index f27ed6e1f..b2a1590b0 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -1167,6 +1167,60 @@ void DeclareFunctionCommand::toStream(std::ostream& out, out, d_func.toString(), sortToTypeNode(d_sort)); } +/* -------------------------------------------------------------------------- */ +/* class DeclareFunctionCommand */ +/* -------------------------------------------------------------------------- */ + +DeclarePoolCommand::DeclarePoolCommand(const std::string& id, + api::Term func, + api::Sort sort, + const std::vector& initValue) + : DeclarationDefinitionCommand(id), + d_func(func), + d_sort(sort), + d_initValue(initValue) +{ +} + +api::Term DeclarePoolCommand::getFunction() const { return d_func; } +api::Sort DeclarePoolCommand::getSort() const { return d_sort; } +const std::vector& DeclarePoolCommand::getInitialValue() const +{ + return d_initValue; +} + +void DeclarePoolCommand::invoke(api::Solver* solver, SymbolManager* sm) +{ + // Notice that the pool is already declared by the parser so that it the + // symbol is bound eagerly. This is analogous to DeclareSygusVarCommand. + // Hence, we do nothing here. + d_commandStatus = CommandSuccess::instance(); +} + +Command* DeclarePoolCommand::clone() const +{ + DeclarePoolCommand* dfc = + new DeclarePoolCommand(d_symbol, d_func, d_sort, d_initValue); + return dfc; +} + +std::string DeclarePoolCommand::getCommandName() const +{ + return "declare-pool"; +} + +void DeclarePoolCommand::toStream(std::ostream& out, + int toDepth, + size_t dag, + OutputLanguage language) const +{ + Printer::getPrinter(language)->toStreamCmdDeclarePool( + out, + d_func.toString(), + sortToTypeNode(d_sort), + termVectorToNodes(d_initValue)); +} + /* -------------------------------------------------------------------------- */ /* class DeclareSortCommand */ /* -------------------------------------------------------------------------- */ diff --git a/src/smt/command.h b/src/smt/command.h index f14d52e94..07dfa2b30 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -425,6 +425,32 @@ class CVC4_EXPORT DeclareFunctionCommand : public DeclarationDefinitionCommand OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class DeclareFunctionCommand */ +class CVC4_EXPORT DeclarePoolCommand : public DeclarationDefinitionCommand +{ + protected: + api::Term d_func; + api::Sort d_sort; + std::vector d_initValue; + + public: + DeclarePoolCommand(const std::string& id, + api::Term func, + api::Sort sort, + const std::vector& initValue); + api::Term getFunction() const; + api::Sort getSort() const; + const std::vector& getInitialValue() const; + + void invoke(api::Solver* solver, SymbolManager* sm) override; + Command* clone() const override; + std::string getCommandName() const override; + void toStream( + std::ostream& out, + int toDepth = -1, + size_t dag = 1, + OutputLanguage language = language::output::LANG_AUTO) const override; +}; /* class DeclarePoolCommand */ + class CVC4_EXPORT DeclareSortCommand : public DeclarationDefinitionCommand { protected: diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 12e0c568d..24d6602e9 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1805,6 +1805,7 @@ set(regress_1_tests regress1/quantifiers/nra-interleave-inst.smt2 regress1/quantifiers/opisavailable-12.smt2 regress1/quantifiers/parametric-lists.smt2 + regress1/quantifiers/pool-example.smt2 regress1/quantifiers/prenex-scholl-smt08_RNDPRE_RNDPRE_4_6.smt2 regress1/quantifiers/psyco-001-bv.smt2 regress1/quantifiers/psyco-107-bv.smt2 diff --git a/test/regress/regress1/quantifiers/pool-example.smt2 b/test/regress/regress1/quantifiers/pool-example.smt2 new file mode 100644 index 000000000..8344f5412 --- /dev/null +++ b/test/regress/regress1/quantifiers/pool-example.smt2 @@ -0,0 +1,17 @@ +; COMMAND-LINE: --pool-inst +; EXPECT: unsat +(set-logic ALL) +(declare-pool L Int ()) + +(declare-fun P (Int) Bool) + +(assert (not (= +(forall ((x Int)) (! (! + (P x) + :skolem-add-to-pool ((- x 100) L)) :pool (L) )) +(forall ((x Int)) (! (! + (P (+ x 100)) + :skolem-add-to-pool ((+ x 100) L)) :pool (L) ) +)))) + +(check-sat) diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp index 361bfa8aa..db950dd7e 100644 --- a/test/unit/api/solver_black.cpp +++ b/test/unit/api/solver_black.cpp @@ -1299,6 +1299,22 @@ TEST_F(TestApiBlackSolver, getInterpolant) ASSERT_TRUE(output.getSort().isBoolean()); } +TEST_F(TestApiBlackSolver, declarePool) +{ + Sort intSort = d_solver.getIntegerSort(); + Sort setSort = d_solver.mkSetSort(intSort); + Term zero = d_solver.mkInteger(0); + Term x = d_solver.mkConst(intSort, "x"); + Term y = d_solver.mkConst(intSort, "y"); + // declare a pool with initial value { 0, x, y } + Term p = d_solver.declarePool("p", intSort, {zero, x, y}); + // pool should have the same sort + ASSERT_TRUE(p.getSort() == setSort); + // cannot pass null sort + Sort nullSort; + ASSERT_THROW(d_solver.declarePool("i", nullSort, {}), CVC5ApiException); +} + TEST_F(TestApiBlackSolver, getOp) { Sort bv32 = d_solver.mkBitVectorSort(32); -- 2.30.2