Towards a new module for enumerating unsat queries via SyGuS.
namespace theory {
namespace quantifiers {
-bool VariadicTrie::add(Node n, const std::vector<Node>& 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<Node>& is) const
-{
- if (!d_data.isNull())
- {
- return true;
- }
- for (const std::pair<const Node, VariadicTrie>& 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;
-}
-
CegisCoreConnective::CegisCoreConnective(Env& env,
QuantifiersState& qs,
QuantifiersInferenceManager& qim,
return true;
}
-void CegisCoreConnective::getModel(SolverEngine& smt,
- std::vector<Node>& vals) const
-{
- for (const Node& v : d_vars)
- {
- Node mv = smt.getValue(v);
- Trace("sygus-ccore-model") << v << " -> " << mv << " ";
- vals.push_back(mv);
- }
-}
-
-bool CegisCoreConnective::getUnsatCore(
- SolverEngine& smt,
- const std::unordered_set<Node>& queryAsserts,
- std::vector<Node>& uasserts) const
-{
- UnsatCore uc = smt.getUnsatCore();
- bool hasQuery = false;
- for (UnsatCore::const_iterator i = uc.begin(); i != uc.end(); ++i)
- {
- Node uassert = *i;
- Trace("sygus-ccore-debug") << " uc " << uassert << std::endl;
- if (queryAsserts.find(uassert) != queryAsserts.end())
- {
- hasQuery = true;
- continue;
- }
- uasserts.push_back(uassert);
- }
- return hasQuery;
-}
-
Result CegisCoreConnective::checkSat(Node n, std::vector<Node>& mvs) const
{
Trace("sygus-ccore-debug") << "...check-sat " << n << "..." << std::endl;
std::unordered_set<Node> queryAsserts;
queryAsserts.insert(ccheck.getFormula());
queryAsserts.insert(d_sc);
- bool hasQuery = getUnsatCore(*checkSol, queryAsserts, uasserts);
+ bool hasQuery =
+ getUnsatCoreFromSubsolver(*checkSol, queryAsserts, uasserts);
// now, check the side condition
bool falseCore = false;
if (!d_sc.isNull())
uasserts.clear();
std::unordered_set<Node> queryAsserts2;
queryAsserts2.insert(d_sc);
- getUnsatCore(*checkSc, queryAsserts2, uasserts);
+ getUnsatCoreFromSubsolver(*checkSc, queryAsserts2, uasserts);
falseCore = true;
}
}
// it does not entail the postcondition, add an assertion that blocks
// the current point
mvs.clear();
- getModel(*checkSol, mvs);
+ getModelFromSubsolver(*checkSol, d_vars, mvs);
// should evaluate to true
Node ean = evaluatePt(an, Node::null(), mvs);
Assert(ean.isConst() && ean.getConst<bool>());
#include "expr/node.h"
#include "expr/node_trie.h"
+#include "expr/variadic_trie.h"
#include "smt/env_obj.h"
#include "theory/quantifiers/sygus/cegis.h"
#include "util/result.h"
namespace theory {
namespace quantifiers {
-/**
- * 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<Node, VariadicTrie> 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<Node>& i);
- /** Is there any data in this trie that is indexed by any subset of is? */
- bool hasSubset(const std::vector<Node>& is) const;
-};
-
/** CegisCoreConnective
*
* A sygus module that is specialized in handling conjectures of the form:
*/
Node d_sc;
//-----------------------------------for SMT engine calls
- /**
- * Assuming smt has just been called to check-sat and returned "SAT", this
- * method adds the model for d_vars to mvs.
- */
- void getModel(SolverEngine& smt, std::vector<Node>& mvs) const;
- /**
- * Assuming smt has just been called to check-sat and returned "UNSAT", this
- * method get the unsat core and adds it to uasserts.
- *
- * The assertions in the argument queryAsserts (which we are not interested
- * in tracking in the unsat core) are excluded from uasserts.
- * If one of the formulas in queryAsserts was in the unsat core, then this
- * method returns true. Otherwise, this method returns false.
- */
- bool getUnsatCore(SolverEngine& smt,
- const std::unordered_set<Node>& queryAsserts,
- std::vector<Node>& uasserts) const;
/**
* Return the result of checking satisfiability of formula n.
* If n was satisfiable, then we store the model for d_vars in mvs.
#include "theory/smt_engine_subsolver.h"
+#include "proof/unsat_core.h"
#include "smt/env.h"
#include "smt/solver_engine.h"
#include "smt/solver_engine_scope.h"
return r;
}
+void getModelFromSubsolver(SolverEngine& smt,
+ const std::vector<Node>& vars,
+ std::vector<Node>& vals)
+{
+ for (const Node& v : vars)
+ {
+ Node mv = smt.getValue(v);
+ vals.push_back(mv);
+ }
+}
+
+bool getUnsatCoreFromSubsolver(SolverEngine& smt,
+ const std::unordered_set<Node>& queryAsserts,
+ std::vector<Node>& uasserts)
+{
+ UnsatCore uc = smt.getUnsatCore();
+ bool hasQuery = false;
+ for (UnsatCore::const_iterator i = uc.begin(); i != uc.end(); ++i)
+ {
+ Node uassert = *i;
+ if (queryAsserts.find(uassert) != queryAsserts.end())
+ {
+ hasQuery = true;
+ continue;
+ }
+ uasserts.push_back(uassert);
+ }
+ return hasQuery;
+}
+
+void getUnsatCoreFromSubsolver(SolverEngine& smt, std::vector<Node>& uasserts)
+{
+ std::unordered_set<Node> queryAsserts;
+ getUnsatCoreFromSubsolver(smt, queryAsserts, uasserts);
+}
+
} // namespace theory
} // namespace cvc5
bool needsTimeout = false,
unsigned long timeout = 0);
+//--------------- utilities
+
+/**
+ * Assuming smt has just been called to check-sat and returned "SAT", this
+ * method adds the model for d_vars to mvs.
+ */
+void getModelFromSubsolver(SolverEngine& smt,
+ const std::vector<Node>& vars,
+ std::vector<Node>& mvs);
+
+/**
+ * Assuming smt has just been called to check-sat and returned "UNSAT", this
+ * method get the unsat core and adds it to uasserts.
+ *
+ * The assertions in the argument queryAsserts (which we are not interested
+ * in tracking in the unsat core) are excluded from uasserts.
+ * If one of the formulas in queryAsserts was in the unsat core, then this
+ * method returns true. Otherwise, this method returns false.
+ */
+bool getUnsatCoreFromSubsolver(SolverEngine& smt,
+ const std::unordered_set<Node>& queryAsserts,
+ std::vector<Node>& uasserts);
+/** Same as above, without query asserts */
+void getUnsatCoreFromSubsolver(SolverEngine& smt, std::vector<Node>& uasserts);
+
} // namespace theory
} // namespace cvc5
projects / cvc5.git / commitdiff