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.
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
{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},
{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},
/* ----------------------------------------------------------------- */
CVC5_API_TRY_CATCH_END;
}
+Term Solver::declarePool(const std::string& symbol,
+ const Sort& sort,
+ const std::vector<Term>& 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<Node> 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());
*/
Term getSeparationNilTerm() const;
+ /**
+ * Declare a symbolic pool of terms with the given initial value.
+ * SMT-LIB:
+ * \verbatim
+ * ( declare-pool <symbol> <sort> ( <term>* ) )
+ * \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<Term>& initValue) const;
/**
* Pop (a) level(s) from the assertion stack.
* SMT-LIB:
* - `Solver::mkTerm(Kind kind, const std::vector<Term>& 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<Term>& 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
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 +
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((<Term?> v).cterm)
+ term.cterm = self.csolver.declarePool(symbol.encode(), sort.csort, niv)
+ return term
+
def pop(self, nscopes=1):
self.csolver.pop(nscopes)
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()); }
/* attributed expressions */
| LPAREN_TOK ATTRIBUTE_TOK term[expr, f2]
- ( attribute[expr, attexpr, attr]
+ ( attribute[expr, attexpr]
{ if( ! attexpr.isNull()) {
patexprs.push_back( attexpr );
}
if(! patexprs.empty()) {
if( !f2.isNull() && f2.getKind()==api::INST_PATTERN_LIST ){
for( size_t i=0; i<f2.getNumChildren(); i++ ){
- if( f2[i].getKind()==api::INST_PATTERN ){
- patexprs.push_back( f2[i] );
- }else{
- std::stringstream ss;
- ss << "warning: rewrite rules do not support " << f2[i]
- << " within instantiation pattern list";
- PARSER_STATE->warning(ss.str());
- }
+ patexprs.push_back( f2[i] );
}
}
expr2 = MK_TERM(api::INST_PATTERN_LIST, patexprs);
/**
* 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;
std::vector<cvc5::api::Term> 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
{
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);
}
| ATTRIBUTE_NAMED_TOK symbolicExpr[sexpr]
{
- attr = std::string(":named");
// notify that expression was given a name
PARSER_STATE->notifyNamedExpression(expr, sexprToString(sexpr));
}
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';
// 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';
printUnknownCommand(out, "declare-fun");
}
+void Printer::toStreamCmdDeclarePool(std::ostream& out,
+ const std::string& id,
+ TypeNode type,
+ const std::vector<Node>& initValue) const
+{
+ printUnknownCommand(out, "declare-pool");
+}
+
void Printer::toStreamCmdDeclareType(std::ostream& out,
TypeNode type) const
{
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<Node>& initValue) const;
/** Print declare-sort command */
virtual void toStreamCmdDeclareType(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<api::Term>& 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<api::Term>& 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 */
/* -------------------------------------------------------------------------- */
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<api::Term> d_initValue;
+
+ public:
+ DeclarePoolCommand(const std::string& id,
+ api::Term func,
+ api::Sort sort,
+ const std::vector<api::Term>& initValue);
+ api::Term getFunction() const;
+ api::Sort getSort() const;
+ const std::vector<api::Term>& 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:
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
--- /dev/null
+; 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)
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);
projects / cvc5.git / commitdiff