summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/smt/set_defaults.cpp99
-rw-r--r--src/smt/set_defaults.h11
-rw-r--r--src/theory/quantifiers/sygus/cegis_unif.cpp4
-rw-r--r--src/theory/quantifiers/sygus/sygus_pbe.cpp2
-rw-r--r--src/theory/quantifiers/sygus/sygus_unif.cpp9
-rw-r--r--src/theory/quantifiers/sygus/sygus_unif.h4
-rw-r--r--src/theory/quantifiers/sygus/sygus_unif_io.cpp27
-rw-r--r--src/theory/quantifiers/sygus/sygus_unif_io.h2
-rw-r--r--src/theory/quantifiers/sygus/sygus_unif_rl.cpp27
-rw-r--r--src/theory/quantifiers/sygus/sygus_unif_rl.h2
-rw-r--r--src/theory/quantifiers/sygus/sygus_unif_strat.cpp3
-rw-r--r--src/theory/quantifiers/sygus/sygus_unif_strat.h6
-rw-r--r--test/regress/CMakeLists.txt3
-rw-r--r--test/regress/regress0/quantifiers/cegqi-needs-justify.smt22
-rw-r--r--test/regress/regress1/nl/issue3647.smt22
-rw-r--r--test/regress/regress1/sygus/issue3648.smt22
16 files changed, 124 insertions, 81 deletions
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 65762a50b..034ca30e2 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -193,13 +193,6 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const
if (opts.smt.solveIntAsBV > 0)
{
- // not compatible with incremental
- if (opts.base.incrementalSolving)
- {
- throw OptionException(
- "solving integers as bitvectors is currently not supported "
- "when solving incrementally.");
- }
// Int to BV currently always eliminates arithmetic completely (or otherwise
// fails). Thus, it is safe to eliminate arithmetic. Also, bit-vectors
// are required.
@@ -253,17 +246,6 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const
if (opts.smt.ackermann)
{
- if (opts.base.incrementalSolving)
- {
- throw OptionException(
- "Incremental Ackermannization is currently not supported.");
- }
-
- if (logic.isQuantified())
- {
- throw LogicException("Cannot use Ackermannization on quantified formula");
- }
-
if (logic.isTheoryEnabled(THEORY_UF))
{
logic = logic.getUnlockedCopy();
@@ -394,25 +376,6 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const
opts.smt.produceAssertions = true;
}
- if (opts.bv.bvAssertInput && opts.smt.produceProofs)
- {
- Notice() << "Disabling bv-assert-input since it is incompatible with proofs."
- << std::endl;
- opts.bv.bvAssertInput = false;
- }
-
- // If proofs are required and the user did not specify a specific BV solver,
- // we make sure to use the proof producing BITBLAST_INTERNAL solver.
- if (opts.smt.produceProofs
- && opts.bv.bvSolver != options::BVSolver::BITBLAST_INTERNAL
- && !opts.bv.bvSolverWasSetByUser
- && opts.bv.bvSatSolver == options::SatSolverMode::MINISAT)
- {
- Notice() << "Forcing internal bit-vector solver due to proof production."
- << std::endl;
- opts.bv.bvSolver = options::BVSolver::BITBLAST_INTERNAL;
- }
-
if (opts.smt.solveBVAsInt != options::SolveBVAsIntMode::OFF)
{
/**
@@ -513,6 +476,18 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const
// widen the logic
widenLogic(logic, opts);
+
+ // check if we have any options that are not supported with quantified logics
+ if (logic.isQuantified())
+ {
+ std::stringstream reasonNoQuant;
+ if (incompatibleWithQuantifiers(opts, reasonNoQuant))
+ {
+ std::stringstream ss;
+ ss << reasonNoQuant.str() << " not supported in quantified logics.";
+ throw OptionException(ss.str());
+ }
+ }
}
void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
@@ -895,7 +870,7 @@ bool SetDefaults::usesSygus(const Options& opts) const
return false;
}
-bool SetDefaults::incompatibleWithProofs(const Options& opts,
+bool SetDefaults::incompatibleWithProofs(Options& opts,
std::ostream& reason) const
{
if (opts.quantifiers.globalNegate)
@@ -912,6 +887,24 @@ bool SetDefaults::incompatibleWithProofs(const Options& opts,
reason << "sygus";
return true;
}
+ // options that are automatically set to support proofs
+ if (opts.bv.bvAssertInput)
+ {
+ Notice()
+ << "Disabling bv-assert-input since it is incompatible with proofs."
+ << std::endl;
+ opts.bv.bvAssertInput = false;
+ }
+ // If proofs are required and the user did not specify a specific BV solver,
+ // we make sure to use the proof producing BITBLAST_INTERNAL solver.
+ if (opts.bv.bvSolver != options::BVSolver::BITBLAST_INTERNAL
+ && !opts.bv.bvSolverWasSetByUser
+ && opts.bv.bvSatSolver == options::SatSolverMode::MINISAT)
+ {
+ Notice() << "Forcing internal bit-vector solver due to proof production."
+ << std::endl;
+ opts.bv.bvSolver = options::BVSolver::BITBLAST_INTERNAL;
+ }
return false;
}
@@ -946,6 +939,11 @@ bool SetDefaults::incompatibleWithIncremental(const LogicInfo& logic,
std::ostream& reason,
std::ostream& suggest) const
{
+ if (opts.smt.ackermann)
+ {
+ reason << "ackermann";
+ return true;
+ }
if (opts.smt.unconstrainedSimp)
{
if (opts.smt.unconstrainedSimpWasSetByUser)
@@ -977,6 +975,11 @@ bool SetDefaults::incompatibleWithIncremental(const LogicInfo& logic,
<< std::endl;
opts.quantifiers.sygusInference = false;
}
+ if (opts.smt.solveIntAsBV > 0)
+ {
+ reason << "solveIntAsBV";
+ return true;
+ }
return false;
}
@@ -1134,6 +1137,26 @@ bool SetDefaults::safeUnsatCores(const Options& opts) const
return opts.smt.unsatCoresMode == options::UnsatCoresMode::ASSUMPTIONS;
}
+bool SetDefaults::incompatibleWithQuantifiers(Options& opts,
+ std::ostream& reason) const
+{
+ if (opts.smt.ackermann)
+ {
+ reason << "ackermann";
+ return true;
+ }
+ if (opts.arith.nlRlvMode != options::NlRlvMode::NONE)
+ {
+ // Theory relevance is incompatible with CEGQI and SyQI, since there is no
+ // appropriate policy for the relevance of counterexample lemmas (when their
+ // guard is entailed to be false, the entire lemma is relevant, not just the
+ // guard). Hence, we throw an option exception if quantifiers are enabled.
+ reason << "--nl-ext-rlv";
+ return true;
+ }
+ return false;
+}
+
void SetDefaults::widenLogic(LogicInfo& logic, Options& opts) const
{
bool needsUf = false;
diff --git a/src/smt/set_defaults.h b/src/smt/set_defaults.h
index 8b83931b5..293f1398d 100644
--- a/src/smt/set_defaults.h
+++ b/src/smt/set_defaults.h
@@ -71,8 +71,11 @@ class SetDefaults
* Return true if proofs must be disabled. This is the case for any technique
* that answers "unsat" without showing a proof of unsatisfiabilty. The output
* stream reason is similar to above.
+ *
+ * Notice this method may modify the options to ensure that we are compatible
+ * with proofs.
*/
- bool incompatibleWithProofs(const Options& opts, std::ostream& reason) const;
+ bool incompatibleWithProofs(Options& opts, std::ostream& reason) const;
/**
* Check whether we should disable models. The output stream reason is similar
* to above.
@@ -89,6 +92,12 @@ class SetDefaults
* techniques that may interfere with producing correct unsat cores.
*/
bool safeUnsatCores(const Options& opts) const;
+ /**
+ * Check if incompatible with quantified formulas. Notice this method may
+ * modify the options to ensure that we are compatible with quantified logics.
+ * The output stream reason is similar to above.
+ */
+ bool incompatibleWithQuantifiers(Options& opts, std::ostream& reason) const;
//------------------------- options setting, prior finalization of logic
/**
* Set defaults pre, which sets all options prior to finalizing the logic.
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index c4d9cbd4a..797aecdab 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -34,7 +34,9 @@ CegisUnif::CegisUnif(QuantifiersState& qs,
QuantifiersInferenceManager& qim,
TermDbSygus* tds,
SynthConjecture* p)
- : Cegis(qs, qim, tds, p), d_sygus_unif(p), d_u_enum_manager(qs, qim, tds, p)
+ : Cegis(qs, qim, tds, p),
+ d_sygus_unif(qs.getEnv(), p),
+ d_u_enum_manager(qs, qim, tds, p)
{
}
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp
index 26621eb96..7601e2117 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.cpp
+++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp
@@ -71,7 +71,7 @@ bool SygusPbe::initialize(Node conj,
for (const Node& c : candidates)
{
Assert(ei->hasExamples(c));
- d_sygus_unif[c].reset(new SygusUnifIo(d_parent));
+ d_sygus_unif[c].reset(new SygusUnifIo(d_env, d_parent));
Trace("sygus-pbe") << "Initialize unif utility for " << c << "..."
<< std::endl;
std::map<Node, std::vector<Node>> strategy_lemmas;
diff --git a/src/theory/quantifiers/sygus/sygus_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp
index 00370ffa2..0787b7913 100644
--- a/src/theory/quantifiers/sygus/sygus_unif.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif.cpp
@@ -27,7 +27,11 @@ namespace cvc5 {
namespace theory {
namespace quantifiers {
-SygusUnif::SygusUnif() : d_tds(nullptr), d_enableMinimality(false) {}
+SygusUnif::SygusUnif(Env& env)
+ : EnvObj(env), d_tds(nullptr), d_enableMinimality(false)
+{
+}
+
SygusUnif::~SygusUnif() {}
void SygusUnif::initializeCandidate(
@@ -39,7 +43,8 @@ void SygusUnif::initializeCandidate(
d_tds = tds;
d_candidates.push_back(f);
// initialize the strategy
- d_strategy[f].initialize(tds, f, enums);
+ d_strategy.emplace(f, SygusUnifStrategy(d_env));
+ d_strategy.at(f).initialize(tds, f, enums);
}
Node SygusUnif::getMinimalTerm(const std::vector<Node>& terms)
diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h
index 2e9e34aa6..80368ea13 100644
--- a/src/theory/quantifiers/sygus/sygus_unif.h
+++ b/src/theory/quantifiers/sygus/sygus_unif.h
@@ -42,10 +42,10 @@ class TermDbSygus;
* Based on the above, solutions can be constructed via calls to
* constructSolution.
*/
-class SygusUnif
+class SygusUnif : protected EnvObj
{
public:
- SygusUnif();
+ SygusUnif(Env& env);
virtual ~SygusUnif();
/** initialize candidate
diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
index 8207a07f2..9626f7af4 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
@@ -509,8 +509,9 @@ void SubsumeTrie::getLeaves(const std::vector<Node>& vals,
getLeavesInternal(vals, pol, v, 0, -2);
}
-SygusUnifIo::SygusUnifIo(SynthConjecture* p)
- : d_parent(p),
+SygusUnifIo::SygusUnifIo(Env& env, SynthConjecture* p)
+ : SygusUnif(env),
+ d_parent(p),
d_check_sol(false),
d_cond_count(0),
d_sol_term_size(0),
@@ -549,7 +550,7 @@ void SygusUnifIo::initializeCandidate(
d_ecache.clear();
SygusUnif::initializeCandidate(tds, f, enums, strategy_lemmas);
// learn redundant operators based on the strategy
- d_strategy[f].staticLearnRedundantOps(strategy_lemmas);
+ d_strategy.at(f).staticLearnRedundantOps(strategy_lemmas);
}
void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
@@ -560,7 +561,7 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
Assert(!d_examples.empty());
Assert(d_examples.size() == d_examples_out.size());
- EnumInfo& ei = d_strategy[c].getEnumInfo(e);
+ EnumInfo& ei = d_strategy.at(c).getEnumInfo(e);
// The explanation for why the current value should be excluded in future
// iterations.
Node exp_exc;
@@ -583,7 +584,7 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
for (const Node& xs : ei.d_enum_slave)
{
Assert(srmap.find(xs) == srmap.end());
- EnumInfo& eiv = d_strategy[c].getEnumInfo(xs);
+ EnumInfo& eiv = d_strategy.at(c).getEnumInfo(xs);
Node templ = eiv.d_template;
if (!templ.isNull())
{
@@ -628,7 +629,7 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
for (unsigned s = 0; s < ei.d_enum_slave.size(); s++)
{
Node xs = ei.d_enum_slave[s];
- EnumInfo& eiv = d_strategy[c].getEnumInfo(xs);
+ EnumInfo& eiv = d_strategy.at(c).getEnumInfo(xs);
EnumCache& ecv = d_ecache[xs];
Trace("sygus-sui-enum") << "Process " << xs << " from " << s << std::endl;
// bool prevIsCover = false;
@@ -829,7 +830,7 @@ Node SygusUnifIo::constructSolutionNode(std::vector<Node>& lemmas)
initializeConstructSol();
initializeConstructSolFor(c);
// call the virtual construct solution method
- Node e = d_strategy[c].getRootEnumerator();
+ Node e = d_strategy.at(c).getRootEnumerator();
Node vcc = constructSol(c, e, role_equal, 1, lemmas);
// if we constructed the solution, and we either did not previously have
// a solution, or the new solution is better (smaller).
@@ -892,10 +893,10 @@ bool SygusUnifIo::useStrContainsEnumeratorExclude(Node e)
<< "Is " << e << " is str.contains exclusion?" << std::endl;
d_use_str_contains_eexc[e] = true;
Node c = d_candidate;
- EnumInfo& ei = d_strategy[c].getEnumInfo(e);
+ EnumInfo& ei = d_strategy.at(c).getEnumInfo(e);
for (const Node& sn : ei.d_enum_slave)
{
- EnumInfo& eis = d_strategy[c].getEnumInfo(sn);
+ EnumInfo& eis = d_strategy.at(c).getEnumInfo(sn);
EnumRole er = eis.getRole();
if (er != enum_io && er != enum_concat_term)
{
@@ -945,7 +946,7 @@ bool SygusUnifIo::getExplanationForEnumeratorExclude(
<< "Check enumerator exclusion for " << e << " -> "
<< d_tds->sygusToBuiltin(v) << " based on str.contains." << std::endl;
std::vector<unsigned> cmp_indices;
- for (unsigned i = 0, size = results.size(); i < size; i++)
+ for (size_t i = 0, size = results.size(); i < size; i++)
{
// If the result is not constant, then it is worthless. It does not
// impact whether the term is excluded.
@@ -955,7 +956,7 @@ bool SygusUnifIo::getExplanationForEnumeratorExclude(
Trace("sygus-sui-cterm-debug")
<< " " << results[i] << " <> " << d_examples_out[i];
Node cont = nm->mkNode(STRING_CONTAINS, d_examples_out[i], results[i]);
- Node contr = Rewriter::rewrite(cont);
+ Node contr = rewrite(cont);
if (contr == d_false)
{
cmp_indices.push_back(i);
@@ -1039,10 +1040,10 @@ Node SygusUnifIo::constructSol(
Trace("sygus-sui-dt-debug") << std::endl;
}
// enumerator type info
- EnumTypeInfo& tinfo = d_strategy[f].getEnumTypeInfo(etn);
+ EnumTypeInfo& tinfo = d_strategy.at(f).getEnumTypeInfo(etn);
// get the enumerator information
- EnumInfo& einfo = d_strategy[f].getEnumInfo(e);
+ EnumInfo& einfo = d_strategy.at(f).getEnumInfo(e);
EnumCache& ecache = d_ecache[e];
diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.h b/src/theory/quantifiers/sygus/sygus_unif_io.h
index fd918c996..79db22ab3 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_io.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_io.h
@@ -265,7 +265,7 @@ class SygusUnifIo : public SygusUnif
friend class UnifContextIo;
public:
- SygusUnifIo(SynthConjecture* p);
+ SygusUnifIo(Env& env, SynthConjecture* p);
~SygusUnifIo();
/** initialize
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
index 09060926b..5af838354 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
@@ -32,8 +32,11 @@ namespace cvc5 {
namespace theory {
namespace quantifiers {
-SygusUnifRl::SygusUnifRl(SynthConjecture* p)
- : d_parent(p), d_useCondPool(false), d_useCondPoolIGain(false)
+SygusUnifRl::SygusUnifRl(Env& env, SynthConjecture* p)
+ : SygusUnif(env),
+ d_parent(p),
+ d_useCondPool(false),
+ d_useCondPoolIGain(false)
{
}
SygusUnifRl::~SygusUnifRl() {}
@@ -55,7 +58,7 @@ void SygusUnifRl::initializeCandidate(
}
// register the strategy
registerStrategy(f, enums, restrictions.d_unused_strategies);
- d_strategy[f].staticLearnRedundantOps(strategy_lemmas, restrictions);
+ d_strategy.at(f).staticLearnRedundantOps(strategy_lemmas, restrictions);
// Copy candidates and check whether CegisUnif for any of them
if (d_unif_candidates.find(f) != d_unif_candidates.end())
{
@@ -118,7 +121,7 @@ Node SygusUnifRl::purifyLemma(Node n,
TNode cand = n[0];
Node tmp = n.substitute(cand, it1->second);
// should be concrete, can just use the rewriter
- nv = Rewriter::rewrite(tmp);
+ nv = rewrite(tmp);
Trace("sygus-unif-rl-purify")
<< "PurifyLemma : model value for " << tmp << " is " << nv << "\n";
}
@@ -231,7 +234,7 @@ Node SygusUnifRl::purifyLemma(Node n,
Trace("sygus-unif-rl-purify")
<< "PurifyLemma : adding model eq " << model_guards.back() << "\n";
}
- nb = Rewriter::rewrite(nb);
+ nb = rewrite(nb);
// every non-top level application of function-to-synthesize must be reduced
// to a concrete constant
Assert(!ensureConst || nb.isConst());
@@ -262,7 +265,7 @@ Node SygusUnifRl::addRefLemma(Node lemma,
model_guards.push_back(plem);
plem = NodeManager::currentNM()->mkNode(OR, model_guards);
}
- plem = Rewriter::rewrite(plem);
+ plem = rewrite(plem);
Trace("sygus-unif-rl-purify") << "Purified lemma : " << plem << "\n";
Trace("sygus-unif-rl-purify") << "Collect new evaluation points...\n";
@@ -316,7 +319,7 @@ bool SygusUnifRl::constructSolution(std::vector<Node>& sols,
}
initializeConstructSolFor(c);
Node v = constructSol(
- c, d_strategy[c].getRootEnumerator(), role_equal, 0, lemmas);
+ c, d_strategy.at(c).getRootEnumerator(), role_equal, 0, lemmas);
if (v.isNull())
{
// we continue trying to build solutions to accumulate potentitial
@@ -337,7 +340,7 @@ Node SygusUnifRl::constructSol(
Trace("sygus-unif-sol") << "ConstructSol: SygusRL : " << e << std::endl;
// retrieve strategy information
TypeNode etn = e.getType();
- EnumTypeInfo& tinfo = d_strategy[f].getEnumTypeInfo(etn);
+ EnumTypeInfo& tinfo = d_strategy.at(f).getEnumTypeInfo(etn);
StrategyNode& snode = tinfo.getStrategyNode(nrole);
if (nrole != role_equal)
{
@@ -412,10 +415,10 @@ void SygusUnifRl::registerStrategy(
{
Trace("sygus-unif-rl-strat")
<< "Strategy for " << f << " is : " << std::endl;
- d_strategy[f].debugPrint("sygus-unif-rl-strat");
+ d_strategy.at(f).debugPrint("sygus-unif-rl-strat");
}
Trace("sygus-unif-rl-strat") << "Register..." << std::endl;
- Node e = d_strategy[f].getRootEnumerator();
+ Node e = d_strategy.at(f).getRootEnumerator();
std::map<Node, std::map<NodeRole, bool>> visited;
registerStrategyNode(f, e, role_equal, visited, enums, unused_strats);
}
@@ -435,7 +438,7 @@ void SygusUnifRl::registerStrategyNode(
}
visited[e][nrole] = true;
TypeNode etn = e.getType();
- EnumTypeInfo& tinfo = d_strategy[f].getEnumTypeInfo(etn);
+ EnumTypeInfo& tinfo = d_strategy.at(f).getEnumTypeInfo(etn);
StrategyNode& snode = tinfo.getStrategyNode(nrole);
for (unsigned j = 0, size = snode.d_strats.size(); j < size; j++)
{
@@ -497,7 +500,7 @@ void SygusUnifRl::registerConditionalEnumerator(Node f,
d_cenum_to_stratpt[cond].clear();
}
// register that this strategy node has a decision tree construction
- d_stratpt_to_dt[e].initialize(cond, this, &d_strategy[f], strategy_index);
+ d_stratpt_to_dt[e].initialize(cond, this, &d_strategy.at(f), strategy_index);
// associate conditional enumerator with strategy node
d_cenum_to_stratpt[cond].push_back(e);
}
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h
index 28506d0bd..11a562d79 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h
@@ -48,7 +48,7 @@ class SynthConjecture;
class SygusUnifRl : public SygusUnif
{
public:
- SygusUnifRl(SynthConjecture* p);
+ SygusUnifRl(Env& env, SynthConjecture* p);
~SygusUnifRl();
/** initialize */
diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
index 15b220c74..10db1ef9e 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
@@ -23,7 +23,6 @@
#include "theory/quantifiers/sygus/sygus_unif.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/quantifiers/term_util.h"
-#include "theory/rewriter.h"
using namespace std;
using namespace cvc5::kind;
@@ -443,7 +442,7 @@ void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole)
teut = children.size() == 1
? children[0]
: nm->mkNode(eut.getKind(), children);
- teut = Rewriter::rewrite(teut);
+ teut = rewrite(teut);
}
else
{
diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.h b/src/theory/quantifiers/sygus/sygus_unif_strat.h
index 11950b0c2..fadf68e3f 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_strat.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_strat.h
@@ -19,7 +19,9 @@
#define CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_STRAT_H
#include <map>
+
#include "expr/node.h"
+#include "smt/env_obj.h"
namespace cvc5 {
namespace theory {
@@ -276,10 +278,10 @@ struct StrategyRestrictions
* the grammar of the function to synthesize f. This tree is represented by
* the above classes.
*/
-class SygusUnifStrategy
+class SygusUnifStrategy : protected EnvObj
{
public:
- SygusUnifStrategy() : d_tds(nullptr) {}
+ SygusUnifStrategy(Env& env) : EnvObj(env), d_tds(nullptr) {}
/** initialize
*
* This initializes this class with function-to-synthesize f. We also call
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 8804563b4..8909bfc06 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2345,7 +2345,6 @@ set(regress_1_tests
regress1/sygus/issue3634.smt2
regress1/sygus/issue3635.smt2
regress1/sygus/issue3644.smt2
- regress1/sygus/issue3648.smt2
regress1/sygus/issue3649.sy
regress1/sygus/issue3802-default-consts.sy
regress1/sygus/issue3839-cond-rewrite.smt2
@@ -2740,6 +2739,8 @@ set(regression_disabled_tests
regress1/sygus/interpol_from_pono_3.smt2
regress1/sygus/interpol_dt.smt2
regress1/sygus/inv_gen_fig8.sy
+ # timeout since nl-rlv is required; however it cannot be used with quantifiers
+ regress1/sygus/issue3648.smt2
# new reconstruct algorithm is slow at reconstructing random constants (see wishue #82)
regress0/sygus/c100.sy
# For the six regressions below, solution terms require rewrites not in
diff --git a/test/regress/regress0/quantifiers/cegqi-needs-justify.smt2 b/test/regress/regress0/quantifiers/cegqi-needs-justify.smt2
index 3aeb38c6e..95deeb141 100644
--- a/test/regress/regress0/quantifiers/cegqi-needs-justify.smt2
+++ b/test/regress/regress0/quantifiers/cegqi-needs-justify.smt2
@@ -1,5 +1,3 @@
-; COMMAND-LINE: --nl-rlv=always --no-sygus-inst
-; EXPECT: unsat
(set-logic NRA)
(set-info :status unsat)
(declare-fun c () Real)
diff --git a/test/regress/regress1/nl/issue3647.smt2 b/test/regress/regress1/nl/issue3647.smt2
index 6c66d2e4c..f863842de 100644
--- a/test/regress/regress1/nl/issue3647.smt2
+++ b/test/regress/regress1/nl/issue3647.smt2
@@ -1,6 +1,6 @@
; COMMAND-LINE: --no-check-models --produce-models --decision=internal --nl-rlv=always
; EXPECT: sat
-(set-logic ALL)
+(set-logic QF_NRAT)
(set-info :status sat)
(assert (distinct (sin 1.0) 0.0))
(check-sat)
diff --git a/test/regress/regress1/sygus/issue3648.smt2 b/test/regress/regress1/sygus/issue3648.smt2
index 2fc1a6115..e7b7547c4 100644
--- a/test/regress/regress1/sygus/issue3648.smt2
+++ b/test/regress/regress1/sygus/issue3648.smt2
@@ -1,5 +1,5 @@
; EXPECT: sat
-; COMMAND-LINE: --sygus-inference --no-check-models --nl-rlv=always
+; COMMAND-LINE: --sygus-inference --no-check-models
(set-logic ALL)
(declare-fun a () Real)
(assert (> a 0.000001))
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback