category = "regular"
long = "sygus-repair-const"
type = "bool"
- default = "true"
+ default = "false"
help = "use approach to repair constants in sygus candidate solutions"
[[option]]
//symmetry breaking
Kind nk = d_tds->getConsNumKind( tn, tindex );
if( options::sygusSymBreak() ){
+ NodeManager* nm = NodeManager::currentNM();
// if less than the maximum depth we consider
if( depth<2 ){
//get children
if( nk==STRING_STRREPL ){
deq_child[0].push_back( 0 );deq_child[1].push_back( 1 );
}
+ // this code adds simple symmetry breaking predicates of the form
+ // d.i != d.j, for example if we are considering an ITE constructor,
+ // we enforce that d.1 != d.2 since otherwise the ITE can be
+ // simplified.
for( unsigned i=0; i<deq_child[0].size(); i++ ){
unsigned c1 = deq_child[0][i];
unsigned c2 = deq_child[1][i];
- if( children[c1].getType()==children[c2].getType() ){
- if( !children[c1].getType().getCardinality().isOne() ){
- sbp_conj.push_back( children[c1].eqNode( children[c2] ).negate() );
+ TypeNode tnc = children[c1].getType();
+ if (tnc == children[c2].getType()
+ && !tnc.getCardinality().isOne())
+ {
+ Node sym_lem_deq = children[c1].eqNode(children[c2]).negate();
+ // must guard if there are symbolic constructors
+ // the issue is that ite( C, _any_constant, _any_constant ) is
+ // a useful solution, since the two instances of _any_constant
+ // can be repaired to different values. Hence, below, we say
+ // e.g. d.i is a symbolic constructor, or it must be different
+ // from d.j.
+ int anyc_cons_num_c = d_tds->getAnyConstantConsNum(tnc);
+ if (anyc_cons_num_c != -1)
+ {
+ const Datatype& cdt =
+ static_cast<DatatypeType>(tnc.toType()).getDatatype();
+ Node guard_val = nm->mkNode(
+ APPLY_CONSTRUCTOR,
+ Node::fromExpr(cdt[anyc_cons_num_c].getConstructor()));
+ Node exp = d_tds->getExplain()->getExplanationForEquality(
+ children[c1], guard_val);
+ sym_lem_deq = nm->mkNode(OR, exp, sym_lem_deq);
}
+ sbp_conj.push_back(sym_lem_deq);
}
}
// if not already solved
if( children_solved.find( j )==children_solved.end() ){
TypeNode tnc = nc.getType();
+ int anyc_cons_num = d_tds->getAnyConstantConsNum(tnc);
const Datatype& cdt = ((DatatypeType)(tnc).toType()).getDatatype();
for( unsigned k=0; k<cdt.getNumConstructors(); k++ ){
Kind nck = d_tds->getConsNumKind(tnc, k);
bool red = false;
// check if the argument is redundant
- if (nck != UNDEFINED_KIND)
+ if (static_cast<int>(k) == anyc_cons_num)
+ {
+ // check if the any constant constructor is redundant at
+ // this argument position
+ // TODO
+ }
+ else if (nck != UNDEFINED_KIND)
{
Trace("sygus-sb-simple-debug")
<< " argument " << j << " " << k << " is : " << nck
}else{
// defined function?
}
+ // explicitly handle "any constant" constructors
+ // if this type admits any constant, then at least one of my children
+ // must not be the "any constant" constructor
+ unsigned dt_index_nargs = dt[tindex].getNumArgs();
+ int tn_ac = d_tds->getAnyConstantConsNum(tn);
+ if (tn_ac != -1 && dt_index_nargs > 0)
+ {
+ std::vector<Node> exp_all_anyc;
+ bool success = true;
+ for (unsigned j = 0; j < dt_index_nargs; j++)
+ {
+ TypeNode ctn = TypeNode::fromType(dt[tindex].getArgType(j));
+ int ctn_ac = d_tds->getAnyConstantConsNum(ctn);
+ if (ctn_ac == -1)
+ {
+ success = false;
+ break;
+ }
+ Node nc = children[j];
+ TypeNode tnc = nc.getType();
+ const Datatype& cdt =
+ static_cast<DatatypeType>(tnc.toType()).getDatatype();
+ exp_all_anyc.push_back(
+ DatatypesRewriter::mkTester(nc, ctn_ac, cdt));
+ }
+ if (success)
+ {
+ Node expaan = exp_all_anyc.size() == 1
+ ? exp_all_anyc[0]
+ : nm->mkNode(AND, exp_all_anyc);
+ expaan = expaan.negate();
+ Trace("sygus-sb-simple-debug")
+ << "Ensure not all any constant: " << expaan << std::endl;
+ sbp_conj.push_back(expaan);
+ }
+ }
}else if( depth==2 ){
if( nk!=UNDEFINED_KIND ){
// commutative operators
void SygusSymBreakNew::addSymBreakLemmasFor( TypeNode tn, Node t, unsigned d, Node a, std::vector< Node >& lemmas ) {
Assert( t.getType()==tn );
Assert( !a.isNull() );
+ Trace("sygus-sb-debug2") << "add sym break lemmas for " << t << " " << d
+ << " " << a << std::endl;
std::map< TypeNode, std::map< unsigned, std::vector< Node > > >::iterator its = d_cache[a].d_sb_lemmas.find( tn );
if( its != d_cache[a].d_sb_lemmas.end() ){
TNode x = getFreeVar( tn );
//get symmetry breaking lemmas for this term
unsigned csz = getSearchSizeForAnchor( a );
int max_sz = ((int)csz) - ((int)d);
+ Trace("sygus-sb-debug2")
+ << "add lemmas up to size " << max_sz << ", which is (search_size) "
+ << csz << " - (depth) " << d << std::endl;
for( std::map< unsigned, std::vector< Node > >::iterator it = its->second.begin(); it != its->second.end(); ++it ){
if( (int)it->first<=max_sz ){
for( unsigned k=0; k<it->second.size(); k++ ){
}
}
}
+ Trace("sygus-sb-debug2") << "...finished." << std::endl;
}
void SygusSymBreakNew::addSymBreakLemma(Node lem,
{
for (const Node& a : anchors)
{
- std::vector<Node> sbl;
- d_tds->getSymBreakLemmas(a, sbl);
- for (const Node& lem : sbl)
+ // is this a registered enumerator?
+ if (d_register_st.find(a) != d_register_st.end())
{
- TypeNode tn = d_tds->getTypeForSymBreakLemma(lem);
- unsigned sz = d_tds->getSizeForSymBreakLemma(lem);
- registerSymBreakLemma(tn, lem, sz, a, lemmas);
+ // symmetry breaking lemmas should only be for enumerators
+ Assert(d_register_st[a]);
+ std::vector<Node> sbl;
+ d_tds->getSymBreakLemmas(a, sbl);
+ for (const Node& lem : sbl)
+ {
+ TypeNode tn = d_tds->getTypeForSymBreakLemma(lem);
+ unsigned sz = d_tds->getSizeForSymBreakLemma(lem);
+ registerSymBreakLemma(tn, lem, sz, a, lemmas);
+ }
+ d_tds->clearSymBreakLemmas(a);
}
}
- d_tds->clearSymBreakLemmas();
if (!lemmas.empty())
{
return;
namespace CVC4 {
namespace theory {
-
-namespace arith {
- class TheoryArith;
-}
-
namespace quantifiers {
class CegqiOutput {
std::vector<Node> candidate_values;
bool constructed_cand = false;
- if (options::sygusRepairConst())
- {
- // have we tried to repair the previous solution?
- // if not, call the repair constant utility
- unsigned ninst = d_cinfo[d_candidates[0]].d_inst.size();
- if (d_repair_index < ninst)
- {
- std::vector<Node> fail_cvs;
- for (const Node& cprog : d_candidates)
- {
- Assert(d_repair_index < d_cinfo[cprog].d_inst.size());
- fail_cvs.push_back(d_cinfo[cprog].d_inst[d_repair_index]);
- }
- d_repair_index++;
- if (d_sygus_rconst->repairSolution(
- d_candidates, fail_cvs, candidate_values))
- {
- constructed_cand = true;
- }
- }
- }
-
// get the model value of the relevant terms from the master module
std::vector<Node> enum_values;
getModelValues(terms, enum_values);
namespace quantifiers {
Cegis::Cegis(QuantifiersEngine* qe, CegConjecture* p)
- : SygusModule(qe, p), d_eval_unfold(nullptr)
+ : SygusModule(qe, p), d_eval_unfold(nullptr), d_using_gr_repair(false)
{
if (options::sygusEvalUnfold())
{
const std::vector<Node>& candidates,
std::vector<Node>& lemmas)
{
+ Trace("cegis") << "Initialize cegis..." << std::endl;
// initialize an enumerator for each candidate
for (unsigned i = 0; i < candidates.size(); i++)
{
- d_tds->registerEnumerator(candidates[i], candidates[i], d_parent);
+ Trace("cegis") << "...register enumerator " << candidates[i];
+ bool do_repair_const = false;
+ if (options::sygusRepairConst())
+ {
+ TypeNode ctn = candidates[i].getType();
+ d_tds->registerSygusType(ctn);
+ if (d_tds->hasSubtermSymbolicCons(ctn))
+ {
+ do_repair_const = true;
+ // remember that we are doing grammar-based repair
+ d_using_gr_repair = true;
+ Trace("cegis") << " (using repair)";
+ }
+ }
+ Trace("cegis") << std::endl;
+ d_tds->registerEnumerator(
+ candidates[i], candidates[i], d_parent, false, do_repair_const);
}
return true;
}
Trace("cegis") << ss.str() << std::endl;
}
}
+ // if we are using grammar-based repair
+ if (d_using_gr_repair)
+ {
+ SygusRepairConst* src = d_parent->getRepairConst();
+ Assert(src != nullptr);
+ // check if any enum_values have symbolic terms that must be repaired
+ bool mustRepair = false;
+ for (const Node& c : enum_values)
+ {
+ if (SygusRepairConst::mustRepair(c))
+ {
+ mustRepair = true;
+ break;
+ }
+ }
+ Trace("cegis") << "...must repair is: " << mustRepair << std::endl;
+ // if the solution contains a subterm that must be repaired
+ if (mustRepair)
+ {
+ std::vector<Node> fail_cvs = enum_values;
+ Assert(candidates.size() == fail_cvs.size());
+ if (src->repairSolution(candidates, fail_cvs, candidate_values))
+ {
+ return true;
+ }
+ // repair solution didn't work, exclude this solution
+ std::vector<Node> exp;
+ for (unsigned i = 0, size = enums.size(); i < size; i++)
+ {
+ d_tds->getExplain()->getExplanationForEquality(
+ enums[i], enum_values[i], exp);
+ }
+ Assert(!exp.empty());
+ Node expn =
+ exp.size() == 1 ? exp[0] : NodeManager::currentNM()->mkNode(AND, exp);
+ lems.push_back(expn.negate());
+ return false;
+ }
+ }
+
// evaluate on refinement lemmas
bool addedEvalLemmas = addEvalLemmas(enums, enum_values);
candidate_values.end(), enum_values.begin(), enum_values.end());
return true;
}
- SygusRepairConst* src = d_parent->getRepairConst();
- if (src != nullptr)
- {
- // it may be repairable
- std::vector<Node> fail_cvs = enum_values;
- Assert(candidates.size() == fail_cvs.size());
- return src->repairSolution(candidates, fail_cvs, candidate_values);
- }
return false;
}
virtual bool processInitialize(Node n,
const std::vector<Node>& candidates,
std::vector<Node>& lemmas);
- /** do cegis-implementation-specific construct candidate
+ /** do cegis-implementation-specific post-processing for construct candidate
*
* satisfiedRl is whether all refinement lemmas are satisfied under the
* substitution { enums -> enum_values }.
* added as refinement lemmas.
*/
std::unordered_set<unsigned> d_cegis_sample_refine;
+
+ //---------------------------------for sygus repair
+ /** are we using grammar-based repair?
+ *
+ * This flag is set ot true if at least one of the enumerators allocated
+ * by this class has been configured to allow model values with symbolic
+ * constructors, such as the "any constant" constructor.
+ */
+ bool d_using_gr_repair;
+ //---------------------------------end for sygus repair
};
} /* CVC4::theory::quantifiers namespace */
#include "printer/sygus_print_callback.h"
#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
+#include "theory/quantifiers/cegqi/ceg_instantiator.h"
#include "theory/quantifiers/sygus/ce_guided_conjecture.h"
#include "theory/quantifiers/sygus/sygus_grammar_red.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
sygus_norm->d_sygus_vars.toExpr(),
dt.getSygusAllowConst(),
dt.getSygusAllowAll());
+ if (dt.getSygusAllowConst())
+ {
+ TypeNode sygus_type = TypeNode::fromType(dt.getSygusType());
+ // must be handled by counterexample-guided instantiation
+ // don't do it for Boolean (not worth the trouble, since it has only
+ // minimal gain (1 any constant vs 2 constructors for true/false), and
+ // we need to do a lot of special symmetry breaking, e.g. for ensuring
+ // any constant constructors are not the 1st children of ITEs.
+ if (CegInstantiator::isCbqiSort(sygus_type) >= CEG_HANDLED
+ && !sygus_type.isBoolean())
+ {
+ Trace("sygus-grammar-normalize") << "...add any constant constructor.\n";
+ // add an "any constant" proxy variable
+ Node av = NodeManager::currentNM()->mkSkolem("_any_constant", sygus_type);
+ // mark that it represents any constant
+ SygusAnyConstAttribute saca;
+ av.setAttribute(saca, true);
+ std::stringstream ss;
+ ss << d_unres_tn << "_any_constant";
+ std::string cname(ss.str());
+ std::vector<Type> empty_arg_types;
+ // we add this constructor first since we use left associative chains
+ // and our symmetry breaking should group any constants together
+ // beneath the same application
+ d_dt.addSygusConstructor(av.toExpr(), cname, empty_arg_types);
+ }
+ }
for (unsigned i = 0, size_d_ops = d_ops.size(); i < size_d_ops; ++i)
{
d_dt.addSygusConstructor(d_ops[i].toExpr(),
class SygusGrammarNorm;
+/** Attribute true for variables that represent any constant */
+struct SygusAnyConstAttributeId
+{
+};
+typedef expr::Attribute<SygusAnyConstAttributeId, bool> SygusAnyConstAttribute;
+
/** Operator position trie class
*
* This data structure stores an unresolved type corresponding to the
#include "smt/smt_engine_scope.h"
#include "smt/smt_statistics_registry.h"
#include "theory/quantifiers/cegqi/ceg_instantiator.h"
+#include "theory/quantifiers/sygus/sygus_grammar_norm.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
using namespace CVC4::kind;
bool SygusRepairConst::repairSolution(const std::vector<Node>& candidates,
const std::vector<Node>& candidate_values,
- std::vector<Node>& repair_cv)
+ std::vector<Node>& repair_cv,
+ bool useConstantsAsHoles)
{
Assert(candidates.size() == candidate_values.size());
Trace("sygus-repair-const")
<< "Getting candidate skeletons : " << std::endl;
}
- NodeManager* nm = NodeManager::currentNM();
std::vector<Node> candidate_skeletons;
std::map<TypeNode, int> free_var_count;
std::vector<Node> sk_vars;
for (unsigned i = 0, size = candidates.size(); i < size; i++)
{
Node cv = candidate_values[i];
- Node skeleton = getSkeleton(cv, free_var_count, sk_vars, sk_vars_to_subs);
+ Node skeleton =
+ getSkeleton(cv, free_var_count, sk_vars, sk_vars_to_subs, useConstantsAsHoles);
if (Trace.isOn("sygus-repair-const"))
{
Printer* p = Printer::getPrinter(options::outputLanguage());
return false;
}
+ NodeManager* nm = NodeManager::currentNM();
Trace("sygus-repair-const") << "Get first-order query..." << std::endl;
Node fo_body = getFoQuery(candidates, candidate_skeletons, sk_vars);
std::vector<Node> sk_sygus_m;
for (const Node& v : sk_vars)
{
+ Assert(d_sk_to_fo.find(v) != d_sk_to_fo.end());
Node fov = d_sk_to_fo[v];
Node fov_m = Node::fromExpr(repcChecker.getValue(fov.toExpr()));
Trace("sygus-repair-const") << " " << fov << " = " << fov_m << std::endl;
return false;
}
-bool SygusRepairConst::isRepairableConstant(Node n)
+bool SygusRepairConst::mustRepair(Node n)
+{
+ std::unordered_set<TNode, TNodeHashFunction> visited;
+ std::vector<TNode> visit;
+ TNode cur;
+ visit.push_back(n);
+ do
+ {
+ cur = visit.back();
+ visit.pop_back();
+ if (visited.find(cur) == visited.end())
+ {
+ visited.insert(cur);
+ Assert(cur.getKind() == APPLY_CONSTRUCTOR);
+ if (isRepairable(cur, false))
+ {
+ return true;
+ }
+ for (const Node& cn : cur)
+ {
+ visit.push_back(cn);
+ }
+ }
+ } while (!visit.empty());
+
+ return false;
+}
+
+bool SygusRepairConst::isRepairable(Node n, bool useConstantsAsHoles)
{
if (n.getKind() != APPLY_CONSTRUCTOR)
{
Assert(tn.isDatatype());
const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
Assert(dt.isSygus());
- if (dt.getSygusAllowConst())
+ Node op = n.getOperator();
+ unsigned cindex = Datatype::indexOf(op.toExpr());
+ if (dt[cindex].getNumArgs() > 0)
{
- Node op = n.getOperator();
- unsigned cindex = Datatype::indexOf(op.toExpr());
- if (dt[cindex].getNumArgs() == 0)
+ return false;
+ }
+ Node sygusOp = Node::fromExpr(dt[cindex].getSygusOp());
+ if (sygusOp.getAttribute(SygusAnyConstAttribute()))
+ {
+ // if it represents "any constant" then it is repairable
+ return true;
+ }
+ if (useConstantsAsHoles && dt.getSygusAllowConst())
+ {
+ if (sygusOp.isConst())
{
- Node sygusOp = Node::fromExpr(dt[cindex].getSygusOp());
- if (sygusOp.isConst())
- {
- return true;
- }
+ // if a constant, it is repairable
+ return true;
}
}
return false;
Node SygusRepairConst::getSkeleton(Node n,
std::map<TypeNode, int>& free_var_count,
std::vector<Node>& sk_vars,
- std::map<Node, Node>& sk_vars_to_subs)
+ std::map<Node, Node>& sk_vars_to_subs,
+ bool useConstantsAsHoles)
{
- if (isRepairableConstant(n))
+ if (isRepairable(n, useConstantsAsHoles))
{
Node sk_var = d_tds->getFreeVarInc(n.getType(), free_var_count);
sk_vars.push_back(sk_var);
for (const Node& cn : cur)
{
Node child;
- // if it is a constant over a type that allows all constants
- if (isRepairableConstant(cn))
+ // if it is repairable
+ if (isRepairable(cn, useConstantsAsHoles))
{
// replace it by the next free variable
child = d_tds->getFreeVarInc(cn.getType(), free_var_count);
Trace("sygus-repair-const-debug") << " ...got : " << body << std::endl;
Trace("sygus-repair-const") << " Introduce first-order vars..." << std::endl;
+ for (const Node& v : sk_vars)
+ {
+ std::map<Node, Node>::iterator itf = d_sk_to_fo.find(v);
+ if (itf == d_sk_to_fo.end())
+ {
+ TypeNode builtinType = d_tds->sygusToBuiltinType(v.getType());
+ Node sk_fov = nm->mkSkolem("k", builtinType);
+ d_sk_to_fo[v] = sk_fov;
+ d_fo_to_sk[sk_fov] = v;
+ Trace("sygus-repair-const-debug")
+ << "Map " << v << " -> " << sk_fov << std::endl;
+ }
+ }
// now, we must replace all terms of the form eval( z_i, t1...tn ) with
// a fresh first-order variable w_i, where z_i is a variable introduced in
// the skeleton inference step (z_i is a variable in sk_vars).
if (std::find(sk_vars.begin(), sk_vars.end(), v) != sk_vars.end())
{
std::map<Node, Node>::iterator itf = d_sk_to_fo.find(v);
- if (itf == d_sk_to_fo.end())
- {
- Node sk_fov = nm->mkSkolem("k", cur.getType());
- d_sk_to_fo[v] = sk_fov;
- d_fo_to_sk[sk_fov] = v;
- visited[cur] = sk_fov;
- Trace("sygus-repair-const-debug")
- << "Map " << v << " -> " << sk_fov << std::endl;
- }
- else
- {
- visited[cur] = itf->second;
- }
+ Assert(itf != d_sk_to_fo.end());
+ visited[cur] = itf->second;
}
}
if (visited[cur].isNull())
if (it == visited.end())
{
visited.insert(cur);
- if (restrictLA && cur.getKind() == NONLINEAR_MULT)
+ Kind ck = cur.getKind();
+ if (restrictLA && (ck == NONLINEAR_MULT || ck == DIVISION))
{
- for (const Node& ccur : cur)
+ for (unsigned j = 0, size = cur.getNumChildren(); j < size; j++)
{
+ Node ccur = cur[j];
std::map<Node, Node>::iterator itf = d_fo_to_sk.find(ccur);
if (itf != d_fo_to_sk.end())
{
- exvar = itf->second;
- return true;
+ if (ck == NONLINEAR_MULT || (ck == DIVISION && j == 1))
+ {
+ exvar = itf->second;
+ return true;
+ }
}
}
return false;
* This module is used to repair portions of candidate solutions. In particular,
* given a synthesis conjecture:
* exists f. forall x. P( f, x )
- * and a candidate solution f = \x. t[x,c] where c are constants, this function
- * checks whether there exists a term of the form \x. t[x,c'] for some constants
- * c' such that:
+ * and a candidate solution f = \x. t[x,r] where r are repairable terms, this
+ * function checks whether there exists a term of the form \x. t[x,c'] for some
+ * constants c' such that:
* forall x. P( (\x. t[x,c']), x ) [***]
* is satisfiable, where notice that the above formula after beta-reduction may
* be one in pure first-order logic in a decidable theory (say linear
* is a solution for the synthesis conjecture associated with this class.
* Moreover, it is the case that
* repair_cv[j] != candidate_values[j], for at least one j.
+ * We always consider applications of the "any constant" constructors in
+ * candidate_values to be repairable. In addition, if the flag
+ * useConstantsAsHoles is true, we consider all constants whose (sygus) type
+ * admit alls constants to be repairable.
*/
bool repairSolution(const std::vector<Node>& candidates,
const std::vector<Node>& candidate_values,
- std::vector<Node>& repair_cv);
+ std::vector<Node>& repair_cv,
+ bool useConstantsAsHoles = false);
+ /** must repair?
+ *
+ * This returns true if n must be repaired for it to be a valid solution.
+ * This corresponds to whether n contains a subterm that is a symbolic
+ * constructor like the "any constant" constructor.
+ */
+ static bool mustRepair(Node n);
private:
/** reference to quantifier engine */
* already registered types.
*/
void registerSygusType(TypeNode tn, std::map<TypeNode, bool>& tprocessed);
- /**
- * Returns true if n is a term of a sygus datatype type that allows all
- * constants, and n encodes a constant. The term n must have a sygus datatype
- * type.
+ /** is repairable?
+ *
+ * This returns true if n can be repaired by this class. In particular, we
+ * return true if n is an "any constant" constructor, or it is a constructor
+ * for a constant in a type that allows all constants and useConstantsAsHoles
+ * is true.
*/
- bool isRepairableConstant(Node n);
+ static bool isRepairable(Node n, bool useConstantsAsHoles);
/** get skeleton
*
- * Returns a skeleton for n, where the subterms of n that are repairable
- * constants are replaced by free variables. Since we are interested in
+ * Returns a skeleton for sygus datatype value n, where the subterms of n that
+ * are repairable are replaced by free variables. Since we are interested in
* returning canonical skeletons, the free variables we use in this
* replacement are taken from TermDbSygus, where we track indices
* in free_var_count. Variables we introduce in this way are added to sk_vars.
* The mapping sk_vars_to_subs contains entries v -> c, where v is a
- * variable in sk_vars, and c is the term in n that it replaced.
+ * variable in sk_vars, and c is the term in n that it replaced. The flag
+ * useConstantsAsHoles affects which terms we consider to be repairable.
*/
Node getSkeleton(Node n,
std::map<TypeNode, int>& free_var_count,
std::vector<Node>& sk_vars,
- std::map<Node, Node>& sk_vars_to_subs);
+ std::map<Node, Node>& sk_vars_to_subs,
+ bool useConstantsAsHoles);
/** get first-order query
*
* This function returns a formula that is equivalent to the negation of the
#include "options/quantifiers_options.h"
#include "theory/arith/arith_msum.h"
#include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/sygus/sygus_grammar_norm.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers_engine.h"
-using namespace std;
using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory::inst;
namespace CVC4 {
namespace theory {
return mkGeneric(dt, c, var_count, pre);
}
+Node TermDbSygus::mkGeneric(const Datatype& dt, int c)
+{
+ std::map<int, Node> pre;
+ return mkGeneric(dt, c, pre);
+}
+
struct SygusToBuiltinAttributeId
{
};
SygusToBuiltinAttribute;
Node TermDbSygus::sygusToBuiltin( Node n, TypeNode tn ) {
+ std::map<TypeNode, int> var_count;
+ return sygusToBuiltin(n, tn, var_count);
+}
+
+Node TermDbSygus::sygusToBuiltin(Node n,
+ TypeNode tn,
+ std::map<TypeNode, int>& var_count)
+{
Assert( n.getType()==tn );
Assert( tn.isDatatype() );
// has it already been computed?
- if (n.hasAttribute(SygusToBuiltinAttribute()))
+ if (var_count.empty() && n.hasAttribute(SygusToBuiltinAttribute()))
{
return n.getAttribute(SygusToBuiltinAttribute());
}
-
Trace("sygus-db-debug") << "SygusToBuiltin : compute for " << n
<< ", type = " << tn << std::endl;
const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
if (n.getKind() == APPLY_CONSTRUCTOR)
{
+ bool var_count_empty = var_count.empty();
unsigned i = Datatype::indexOf(n.getOperator().toExpr());
Assert(n.getNumChildren() == dt[i].getNumArgs());
- std::map<TypeNode, int> var_count;
std::map<int, Node> pre;
for (unsigned j = 0, size = n.getNumChildren(); j < size; j++)
{
- pre[j] = sygusToBuiltin(n[j], getArgType(dt[i], j));
+ // if the child is a symbolic constructor, do not include it
+ if (!isSymbolicConsApp(n[j]))
+ {
+ pre[j] = sygusToBuiltin(
+ n[j], TypeNode::fromType(dt[i].getArgType(j)), var_count);
+ }
}
Node ret = mkGeneric(dt, i, var_count, pre);
Trace("sygus-db-debug")
<< "SygusToBuiltin : Generic is " << ret << std::endl;
- n.setAttribute(SygusToBuiltinAttribute(), ret);
+ // cache if we had a fresh variable count
+ if (var_count_empty)
+ {
+ n.setAttribute(SygusToBuiltinAttribute(), ret);
+ }
return ret;
}
if (n.hasAttribute(SygusPrintProxyAttribute()))
{
for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
{
- registerSygusType(getArgType(dt[i], j));
+ TypeNode ctn = TypeNode::fromType(dt[i].getArgType(j));
+ registerSygusType(ctn);
+ // carry type attributes
+ if (d_has_subterm_sym_cons.find(ctn)
+ != d_has_subterm_sym_cons.end())
+ {
+ d_has_subterm_sym_cons[tn] = true;
+ }
}
}
//iterate over constructors
<< std::endl;
}
}
+ // symbolic constructors
+ if (n.getAttribute(SygusAnyConstAttribute()))
+ {
+ d_sym_cons_any_constant[tn] = i;
+ d_has_subterm_sym_cons[tn] = true;
+ }
// TODO (as part of #1170): we still do not properly catch type
// errors in sygus grammars for arguments of builtin operators.
// The challenge is that we easily ask for expected argument types of
// ensure that terms that this constructor encodes are
// of the type specified in the datatype. This will fail if
// e.g. bitvector-and is a constructor of an integer grammar.
- std::map<int, Node> pre;
- Node g = mkGeneric(dt, i, pre);
+ Node g = mkGeneric(dt, i);
TypeNode gtn = g.getType();
CVC4_CHECK(gtn.isSubtypeOf(btn))
<< "Sygus datatype " << dt.getName()
<< " encodes terms that are not of type " << btn << std::endl;
}
+ // compute min type depth information
+ computeMinTypeDepthInternal(tn, tn, 0);
}
}
}
void TermDbSygus::registerEnumerator(Node e,
Node f,
CegConjecture* conj,
- bool mkActiveGuard)
+ bool mkActiveGuard,
+ bool useSymbolicCons)
{
if (d_enum_to_conjecture.find(e) != d_enum_to_conjecture.end())
{
}
Trace("sygus-db") << "Register enumerator : " << e << std::endl;
// register its type
- registerSygusType(e.getType());
+ TypeNode et = e.getType();
+ registerSygusType(et);
d_enum_to_conjecture[e] = conj;
d_enum_to_synth_fun[e] = f;
+ NodeManager* nm = NodeManager::currentNM();
if( mkActiveGuard ){
// make the guard
- Node eg = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "eG", NodeManager::currentNM()->booleanType() ) );
+ Node eg = Rewriter::rewrite(nm->mkSkolem("eG", nm->booleanType()));
eg = d_quantEngine->getValuation().ensureLiteral( eg );
AlwaysAssert( !eg.isNull() );
d_quantEngine->getOutputChannel().requirePhase( eg, true );
//add immediate lemma
- Node lem = NodeManager::currentNM()->mkNode( OR, eg, eg.negate() );
+ Node lem = nm->mkNode(OR, eg, eg.negate());
Trace("cegqi-lemma") << "Cegqi::Lemma : enumerator : " << lem << std::endl;
d_quantEngine->getOutputChannel().lemma( lem );
d_enum_to_active_guard[e] = eg;
}
+
+ // depending on if we are using symbolic constructors, introduce symmetry
+ // breaking lemma templates for each relevant subtype of the grammar
+ std::map<TypeNode, std::map<TypeNode, unsigned> >::iterator it =
+ d_min_type_depth.find(et);
+ Assert(it != d_min_type_depth.end());
+ // for each type of subterm of this enumerator
+ for (const std::pair<const TypeNode, unsigned>& st : it->second)
+ {
+ std::vector<unsigned> rm_indices;
+ TypeNode stn = st.first;
+ Assert(stn.isDatatype());
+ const Datatype& dt = static_cast<DatatypeType>(stn.toType()).getDatatype();
+ std::map<TypeNode, unsigned>::iterator itsa =
+ d_sym_cons_any_constant.find(stn);
+ if (itsa != d_sym_cons_any_constant.end())
+ {
+ if (!useSymbolicCons)
+ {
+ // do not use the symbolic constructor
+ rm_indices.push_back(itsa->second);
+ }
+ else
+ {
+ // can remove all other concrete constant constructors
+ for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
+ {
+ if (i != itsa->second)
+ {
+ Node c_op = getConsNumConst(stn, i);
+ if (!c_op.isNull())
+ {
+ rm_indices.push_back(i);
+ }
+ }
+ }
+ }
+ }
+ for (unsigned& rindex : rm_indices)
+ {
+ // make the apply-constructor corresponding to an application of the
+ // "any constant" constructor
+ Node exc_val = nm->mkNode(APPLY_CONSTRUCTOR,
+ Node::fromExpr(dt[rindex].getConstructor()));
+ // should not include the constuctor in any subterm
+ Node x = getFreeVar(stn, 0);
+ Trace("sygus-db") << "Construct symmetry breaking lemma from " << x
+ << " == " << exc_val << std::endl;
+ Node lem = getExplain()->getExplanationForEquality(x, exc_val);
+ lem = lem.negate();
+ Trace("cegqi-lemma")
+ << "Cegqi::Lemma : exclude symbolic cons lemma (template) : " << lem
+ << std::endl;
+ // the size of the subterm we are blocking is the weight of the
+ // constructor (usually zero)
+ registerSymBreakLemma(e, lem, stn, dt[rindex].getWeight());
+ }
+ }
}
bool TermDbSygus::isEnumerator(Node e) const
return it->second;
}
-void TermDbSygus::clearSymBreakLemmas()
-{
- d_enum_to_sb_lemmas.clear();
- d_sb_lemma_to_type.clear();
- d_sb_lemma_to_size.clear();
-}
+void TermDbSygus::clearSymBreakLemmas(Node e) { d_enum_to_sb_lemmas.erase(e); }
-bool TermDbSygus::isRegistered( TypeNode tn ) {
+bool TermDbSygus::isRegistered(TypeNode tn) const
+{
return d_register.find( tn )!=d_register.end();
}
unsigned TermDbSygus::getMinTypeDepth( TypeNode root_tn, TypeNode tn ){
std::map< TypeNode, unsigned >::iterator it = d_min_type_depth[root_tn].find( tn );
if( it==d_min_type_depth[root_tn].end() ){
- computeMinTypeDepthInternal( root_tn, root_tn, 0 );
Assert( d_min_type_depth[root_tn].find( tn )!=d_min_type_depth[root_tn].end() );
return d_min_type_depth[root_tn][tn];
}else{
}
}
+int TermDbSygus::getAnyConstantConsNum(TypeNode tn) const
+{
+ Assert(isRegistered(tn));
+ std::map<TypeNode, unsigned>::const_iterator itt =
+ d_sym_cons_any_constant.find(tn);
+ if (itt != d_sym_cons_any_constant.end())
+ {
+ return static_cast<int>(itt->second);
+ }
+ return -1;
+}
+
+bool TermDbSygus::hasSubtermSymbolicCons(TypeNode tn) const
+{
+ return d_has_subterm_sym_cons.find(tn) != d_has_subterm_sym_cons.end();
+}
+
+bool TermDbSygus::isSymbolicConsApp(Node n) const
+{
+ if (n.getKind() != APPLY_CONSTRUCTOR)
+ {
+ return false;
+ }
+ TypeNode tn = n.getType();
+ const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
+ Assert(dt.isSygus());
+ unsigned cindex = Datatype::indexOf(n.getOperator().toExpr());
+ Node sygusOp = Node::fromExpr(dt[cindex].getSygusOp());
+ // it is symbolic if it represents "any constant"
+ return sygusOp.getAttribute(SygusAnyConstAttribute());
+}
+
Node TermDbSygus::minimizeBuiltinTerm( Node n ) {
if( ( n.getKind()==EQUAL || n.getKind()==LEQ || n.getKind()==LT || n.getKind()==GEQ || n.getKind()==GT ) &&
( n[0].getType().isInteger() || n[0].getType().isReal() ) ){
cc.insert( cc.end(), args.begin(), args.end() );
pre[j] = NodeManager::currentNM()->mkNode( kind::APPLY_UF, cc );
}
- std::map< TypeNode, int > var_count;
- Node ret = mkGeneric( dt, i, var_count, pre );
+ Node ret = mkGeneric(dt, i, pre);
// if it is a variable, apply the substitution
if( ret.getKind()==kind::BOUND_VARIABLE ){
Assert( ret.hasAttribute(SygusVarNumAttribute()) );
* conj : the conjecture that the enumeration of e is for.
* f : the synth-fun that the enumeration of e is for.
* mkActiveGuard : whether we want to make an active guard for e
- * (see d_enum_to_active_guard).
+ * (see d_enum_to_active_guard),
+ * useSymbolicCons : whether we want model values for e to include symbolic
+ * constructors like the "any constant" variable.
*
* Notice that enumerator e may not be one-to-one with f in
* synthesis-through-unification approaches (e.g. decision tree construction
void registerEnumerator(Node e,
Node f,
CegConjecture* conj,
- bool mkActiveGuard = false);
+ bool mkActiveGuard = false,
+ bool useSymbolicCons = false);
/** is e an enumerator registered with this class? */
bool isEnumerator(Node e) const;
/** return the conjecture e is associated with */
TypeNode getTypeForSymBreakLemma(Node lem) const;
/** Get the minimum size of terms symmetry breaking lemma lem applies to */
unsigned getSizeForSymBreakLemma(Node lem) const;
- /** Clear information about symmetry breaking lemmas */
- void clearSymBreakLemmas();
+ /** Clear information about symmetry breaking lemmas for enumerator e */
+ void clearSymBreakLemmas(Node e);
//------------------------------end enumerators
//-----------------------------conversion from sygus to builtin
std::map<int, Node>& pre);
/** same as above, but with empty var_count */
Node mkGeneric(const Datatype& dt, int c, std::map<int, Node>& pre);
+ /** same as above, but with empty pre */
+ Node mkGeneric(const Datatype& dt, int c);
/** sygus to builtin
*
* Given a sygus datatype term n of type tn, this function returns its analog,
* that is, the term that n encodes.
+ *
+ * Notice that each occurrence of a symbolic constructor application is
+ * replaced by a unique variable. To track counters for introducing unique
+ * variables, we use the var_count map.
*/
Node sygusToBuiltin(Node n, TypeNode tn);
+ Node sygusToBuiltin(Node n, TypeNode tn, std::map<TypeNode, int>& var_count);
/** same as above, but without tn */
Node sygusToBuiltin(Node n) { return sygusToBuiltin(n, n.getType()); }
/** evaluate builtin
Node d_true;
Node d_false;
-private:
+ private:
+ /** computes the map d_min_type_depth */
void computeMinTypeDepthInternal( TypeNode root_tn, TypeNode tn, unsigned type_depth );
bool involvesDivByZero( Node n, std::map< Node, bool >& visited );
std::map<TypeNode, std::map<Node, Node> > d_semantic_skolem;
// grammar information
// root -> type -> _
+ /**
+ * For each sygus type t1, this maps datatype types t2 to the smallest size of
+ * a term of type t1 that includes t2 as a subterm. For example, for grammar:
+ * A -> B+B | 0 | B-D
+ * B -> C+C
+ * ...
+ * we have that d_min_type_depth[A] = { A -> 0, B -> 1, C -> 2, D -> 1 }.
+ */
std::map<TypeNode, std::map<TypeNode, unsigned> > d_min_type_depth;
// std::map< TypeNode, std::map< Node, std::map< std::map< int, bool > > >
// d_consider_const;
std::map<TypeNode, std::map<unsigned, unsigned> > d_min_cons_term_size;
/** a cache for getSelectorWeight */
std::map<TypeNode, std::map<Node, unsigned> > d_sel_weight;
+ /**
+ * For each sygus type, the index of the "any constant" constructor, if it
+ * has one.
+ */
+ std::map<TypeNode, unsigned> d_sym_cons_any_constant;
+ /**
+ * Whether any subterm of this type contains a symbolic constructor. This
+ * corresponds to whether sygus repair techniques will ever have any effect
+ * for this type.
+ */
+ std::map<TypeNode, bool> d_has_subterm_sym_cons;
public: // general sygus utilities
- bool isRegistered( TypeNode tn );
+ bool isRegistered(TypeNode tn) const;
// get the minimum depth of type in its parent grammar
unsigned getMinTypeDepth( TypeNode root_tn, TypeNode tn );
// get the minimum size for a constructor term
int getFirstArgOccurrence( const DatatypeConstructor& c, TypeNode tn );
/** is type match */
bool isTypeMatch( const DatatypeConstructor& c1, const DatatypeConstructor& c2 );
+ /**
+ * Get the index of the "any constant" constructor of type tn if it has one,
+ * or returns -1 otherwise.
+ */
+ int getAnyConstantConsNum(TypeNode tn) const;
+ /** has subterm symbolic constructor
+ *
+ * Returns true if any subterm of type tn can be a symbolic constructor.
+ */
+ bool hasSubtermSymbolicCons(TypeNode tn) const;
+ /** return whether n is an application of a symbolic constructor */
+ bool isSymbolicConsApp(Node n) const;
TypeNode getSygusTypeForVar( Node v );
Node sygusSubstituted( TypeNode tn, Node n, std::vector< Node >& args );
regress0/expect/scrub.03.smt2 \
regress0/expect/scrub.04.smt2 \
regress0/expect/scrub.06.cvc \
- regress0/expect/scrub.07.sy \
regress0/expect/scrub.08.sy \
regress0/expect/scrub.09.p \
regress0/flet.smt \
regress0/decision/wchains010ue.smt.expect \
regress0/expect/scrub.01.smt.expect \
regress0/expect/scrub.03.smt2.expect \
- regress0/expect/scrub.07.sy.expect \
regress0/quantifiers/bug291.smt2.expect \
regress0/uflia/check02.smt2.expect \
regress0/uflia/check03.smt2.expect \
+++ /dev/null
-; COMMAND-LINE: --cegqi-si=all --sygus-out=status
-(set-logic LIA)
-(declare-var n Int)
-
-(synth-fun f ((n Int)) Int)
-(constraint (= (/ n n) 1))
-(check-synth)
+++ /dev/null
-% SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/'
-% EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic.
-% EXPECT: The fact in question: TERM
-% EXPECT: ")
-% EXIT: 1
; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --sygus-out=status --sygus-repair-const
(set-logic LIA)
(synth-inv inv-f ((y Int) (z Int) (c Int)))
(inv-constraint inv-f pre-f trans-f post-f)
+; needs --sygus-repair-const, since easy solution involves the constant 4608
+
(check-synth)
projects / cvc5.git / commitdiff