summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/CMakeLists.txt2
-rw-r--r--src/api/cpp/cvc5.cpp24
-rw-r--r--src/api/cpp/cvc5.h13
-rw-r--r--src/api/cpp/cvc5_kind.h28
-rw-r--r--src/api/python/cvc4.pxd1
-rw-r--r--src/api/python/cvc4.pxi8
-rw-r--r--src/parser/smt2/Smt2.g47
-rw-r--r--src/printer/printer.cpp8
-rw-r--r--src/printer/printer.h5
-rw-r--r--src/smt/command.cpp54
-rw-r--r--src/smt/command.h26
11 files changed, 198 insertions, 18 deletions
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<Kind, cvc5::Kind, KindHashFunction> 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, Kind, cvc5::kind::KindHashFunction>
{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<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());
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
@@ -3567,6 +3567,19 @@ class CVC4_EXPORT Solver
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:
* \verbatim
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<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
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((<Term?> 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<cvc5::Command>* 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; 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);
@@ -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<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
@@ -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<Node>& 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<Node>& 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
@@ -1168,6 +1168,60 @@ void DeclareFunctionCommand::toStream(std::ostream& out,
}
/* -------------------------------------------------------------------------- */
+/* 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 */
/* -------------------------------------------------------------------------- */
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<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:
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback