preprocessing/passes/sort_infer.h
preprocessing/passes/static_learning.cpp
preprocessing/passes/static_learning.h
+ preprocessing/passes/sygus_abduct.cpp
+ preprocessing/passes/sygus_abduct.h
preprocessing/passes/sygus_inference.cpp
preprocessing/passes/sygus_inference.h
preprocessing/passes/symmetry_breaker.cpp
read_only = false
help = "attempt to preprocess arbitrary inputs to sygus conjectures"
+[[option]]
+ name = "sygusAbduct"
+ category = "regular"
+ long = "sygus-abduct"
+ type = "bool"
+ default = "false"
+ read_only = false
+ help = "compute abductions using sygus"
+
[[option]]
name = "ceGuidedInst"
category = "regular"
default = "false"
help = "compute backwards filtering to compute whether previous solutions are filtered based on later ones"
+
[[option]]
name = "sygusExprMinerCheckUseExport"
category = "expert"
--- /dev/null
+/********************* */
+/*! \file sygus_abduct.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of sygus abduction preprocessing pass, which
+ ** transforms an arbitrary input into an abduction problem.
+ **/
+
+#include "preprocessing/passes/sygus_abduct.h"
+
+#include "expr/node_algorithm.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
+#include "smt/smt_statistics_registry.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/quantifiers_rewriter.h"
+#include "theory/quantifiers/term_util.h"
+#include "theory/rewriter.h"
+
+using namespace std;
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+SygusAbduct::SygusAbduct(PreprocessingPassContext* preprocContext)
+ : PreprocessingPass(preprocContext, "sygus-abduct"){};
+
+PreprocessingPassResult SygusAbduct::applyInternal(
+ AssertionPipeline* assertionsToPreprocess)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ Trace("sygus-abduct") << "Run sygus abduct..." << std::endl;
+
+ Trace("sygus-abduct-debug") << "Collect symbols..." << std::endl;
+ std::unordered_set<Node, NodeHashFunction> symset;
+ std::vector<Node>& asserts = assertionsToPreprocess->ref();
+ // do we have any assumptions, e.g. via check-sat-assuming?
+ bool usingAssumptions = (assertionsToPreprocess->getNumAssumptions() > 0);
+ // The following is our set of "axioms". We construct this set only when the
+ // usingAssumptions (above) is true. In this case, our input formula is
+ // partitioned into Fa ^ Fc as described in the header of this class, where:
+ // - The conjunction of assertions marked as assumptions are the negated
+ // conjecture Fc, and
+ // - The conjunction of all other assertions are the axioms Fa.
+ std::vector<Node> axioms;
+ for (size_t i = 0, size = asserts.size(); i < size; i++)
+ {
+ expr::getSymbols(asserts[i], symset);
+ // if we are not an assumption, add it to the set of axioms
+ if (usingAssumptions && i < assertionsToPreprocess->getAssumptionsStart())
+ {
+ axioms.push_back(asserts[i]);
+ }
+ }
+ Trace("sygus-abduct-debug")
+ << "...finish, got " << symset.size() << " symbols." << std::endl;
+
+ Trace("sygus-abduct-debug") << "Setup symbols..." << std::endl;
+ std::vector<Node> syms;
+ std::vector<Node> vars;
+ std::vector<Node> varlist;
+ std::vector<TypeNode> varlistTypes;
+ for (const Node& s : symset)
+ {
+ TypeNode tn = s.getType();
+ if (tn.isFirstClass())
+ {
+ std::stringstream ss;
+ ss << s;
+ Node var = nm->mkBoundVar(tn);
+ syms.push_back(s);
+ vars.push_back(var);
+ Node vlv = nm->mkBoundVar(ss.str(), tn);
+ varlist.push_back(vlv);
+ varlistTypes.push_back(tn);
+ }
+ }
+ Trace("sygus-abduct-debug") << "...finish" << std::endl;
+
+ Trace("sygus-abduct-debug") << "Make abduction predicate..." << std::endl;
+ // make the abduction predicate to synthesize
+ TypeNode abdType = varlistTypes.empty() ? nm->booleanType()
+ : nm->mkPredicateType(varlistTypes);
+ Node abd = nm->mkBoundVar("A", abdType);
+ Trace("sygus-abduct-debug") << "...finish" << std::endl;
+
+ Trace("sygus-abduct-debug") << "Make abduction predicate app..." << std::endl;
+ std::vector<Node> achildren;
+ achildren.push_back(abd);
+ achildren.insert(achildren.end(), vars.begin(), vars.end());
+ Node abdApp = vars.empty() ? abd : nm->mkNode(APPLY_UF, achildren);
+ Trace("sygus-abduct-debug") << "...finish" << std::endl;
+
+ Trace("sygus-abduct-debug") << "Set attributes..." << std::endl;
+ // set the sygus bound variable list
+ Node abvl = nm->mkNode(BOUND_VAR_LIST, varlist);
+ abd.setAttribute(theory::SygusSynthFunVarListAttribute(), abvl);
+ Trace("sygus-abduct-debug") << "...finish" << std::endl;
+
+ Trace("sygus-abduct-debug") << "Make conjecture body..." << std::endl;
+ Node input = asserts.size() == 1 ? asserts[0] : nm->mkNode(AND, asserts);
+ input = input.substitute(syms.begin(), syms.end(), vars.begin(), vars.end());
+ // A(x) => ~input( x )
+ input = nm->mkNode(OR, abdApp.negate(), input.negate());
+ Trace("sygus-abduct-debug") << "...finish" << std::endl;
+
+ Trace("sygus-abduct-debug") << "Make conjecture..." << std::endl;
+ Node res = input.negate();
+ if (!vars.empty())
+ {
+ Node bvl = nm->mkNode(BOUND_VAR_LIST, vars);
+ // exists x. ~( A( x ) => ~input( x ) )
+ res = nm->mkNode(EXISTS, bvl, res);
+ }
+ // sygus attribute
+ Node sygusVar = nm->mkSkolem("sygus", nm->booleanType());
+ theory::SygusAttribute ca;
+ sygusVar.setAttribute(ca, true);
+ Node instAttr = nm->mkNode(INST_ATTRIBUTE, sygusVar);
+ std::vector<Node> iplc;
+ iplc.push_back(instAttr);
+ if (!axioms.empty())
+ {
+ Node aconj = axioms.size() == 1 ? axioms[0] : nm->mkNode(AND, axioms);
+ aconj =
+ aconj.substitute(syms.begin(), syms.end(), vars.begin(), vars.end());
+ Trace("sygus-abduct") << "---> Assumptions: " << aconj << std::endl;
+ Node sc = nm->mkNode(AND, aconj, abdApp);
+ Node vbvl = nm->mkNode(BOUND_VAR_LIST, vars);
+ sc = nm->mkNode(EXISTS, vbvl, sc);
+ Node sygusScVar = nm->mkSkolem("sygus_sc", nm->booleanType());
+ sygusScVar.setAttribute(theory::SygusSideConditionAttribute(), sc);
+ instAttr = nm->mkNode(INST_ATTRIBUTE, sygusScVar);
+ // build in the side condition
+ // exists x. A( x ) ^ input_axioms( x )
+ // as an additional annotation on the sygus conjecture. In other words,
+ // the abducts A we procedure must be consistent with our axioms.
+ iplc.push_back(instAttr);
+ }
+ Node instAttrList = nm->mkNode(INST_PATTERN_LIST, iplc);
+
+ Node fbvl = nm->mkNode(BOUND_VAR_LIST, abd);
+
+ // forall A. exists x. ~( A( x ) => ~input( x ) )
+ res = nm->mkNode(FORALL, fbvl, res, instAttrList);
+ Trace("sygus-abduct-debug") << "...finish" << std::endl;
+
+ res = theory::Rewriter::rewrite(res);
+
+ Trace("sygus-abduct") << "Generate: " << res << std::endl;
+
+ Node trueNode = nm->mkConst(true);
+
+ assertionsToPreprocess->replace(0, res);
+ for (size_t i = 1, size = assertionsToPreprocess->size(); i < size; ++i)
+ {
+ assertionsToPreprocess->replace(i, trueNode);
+ }
+
+ return PreprocessingPassResult::NO_CONFLICT;
+}
+
+} // namespace passes
+} // namespace preprocessing
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file sygus_abduct.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Sygus abduction preprocessing pass, which transforms an arbitrary
+ ** input into an abduction problem.
+ **/
+
+#ifndef __CVC4__PREPROCESSING__PASSES__SYGUS_ABDUCT_H
+#define __CVC4__PREPROCESSING__PASSES__SYGUS_ABDUCT_H
+
+#include "preprocessing/preprocessing_pass.h"
+#include "preprocessing/preprocessing_pass_context.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+/** SygusAbduct
+ *
+ * A preprocessing utility that turns a set of quantifier-free assertions into
+ * a sygus conjecture that encodes an abduction problem. In detail, if our
+ * input formula is F( x ) for free symbols x, then we construct the sygus
+ * conjecture:
+ *
+ * exists A. forall x. ( A( x ) => ~F( x ) )
+ *
+ * where A( x ) is a predicate over the free symbols of our input. In other
+ * words, A( x ) is a sufficient condition for showing ~F( x ).
+ *
+ * Another way to view this is A( x ) is any condition such that A( x ) ^ F( x )
+ * is unsatisfiable.
+ *
+ * A common use case is to find the weakest such A that meets the above
+ * specification. We do this by streaming solutions (sygus-stream) for A
+ * while filtering stronger solutions (sygus-filter-sol=strong). These options
+ * are enabled by default when this preprocessing class is used (sygus-abduct).
+ *
+ * If the input F( x ) is partitioned into axioms Fa and negated conjecture Fc
+ * Fa( x ) ^ Fc( x ), then the sygus conjecture we construct is:
+ *
+ * exists A. ( exists y. A( y ) ^ Fa( y ) ) ^ forall x. ( A( x ) => ~F( x ) )
+ *
+ * In other words, A( y ) must be consistent with our axioms Fa and imply
+ * ~F( x ). We encode this conjecture using SygusSideConditionAttribute.
+ */
+class SygusAbduct : public PreprocessingPass
+{
+ public:
+ SygusAbduct(PreprocessingPassContext* preprocContext);
+
+ protected:
+ /**
+ * Replaces the set of assertions by an abduction sygus problem described
+ * above.
+ */
+ PreprocessingPassResult applyInternal(
+ AssertionPipeline* assertionsToPreprocess) override;
+};
+
+} // namespace passes
+} // namespace preprocessing
+} // namespace CVC4
+
+#endif /* __CVC4__PREPROCESSING__PASSES__SYGUS_ABDUCT_H_ */
#include "preprocessing/passes/sep_skolem_emp.h"
#include "preprocessing/passes/sort_infer.h"
#include "preprocessing/passes/static_learning.h"
+#include "preprocessing/passes/sygus_abduct.h"
#include "preprocessing/passes/sygus_inference.h"
#include "preprocessing/passes/symmetry_breaker.h"
#include "preprocessing/passes/symmetry_detect.h"
registerPassInfo("synth-rr", callCtor<SynthRewRulesPass>);
registerPassInfo("real-to-int", callCtor<RealToInt>);
registerPassInfo("sygus-infer", callCtor<SygusInference>);
+ registerPassInfo("sygus-abduct", callCtor<SygusAbduct>);
registerPassInfo("bv-to-bool", callCtor<BVToBool>);
registerPassInfo("bv-intro-pow2", callCtor<BvIntroPow2>);
registerPassInfo("sort-inference", callCtor<SortInferencePass>);
d_defineCommands(),
d_logic(),
d_originalOptions(),
+ d_isInternalSubsolver(false),
d_pendingPops(0),
d_fullyInited(false),
d_problemExtended(false),
}
// sygus inference may require datatypes
- if (options::sygusInference() || options::sygusRewSynthInput())
+ if (!d_isInternalSubsolver)
{
- d_logic = d_logic.getUnlockedCopy();
- // sygus requires arithmetic, datatypes and quantifiers
- d_logic.enableTheory(THEORY_ARITH);
- d_logic.enableTheory(THEORY_DATATYPES);
- d_logic.enableTheory(THEORY_QUANTIFIERS);
- d_logic.lock();
- // since we are trying to recast as sygus, we assume the input is sygus
- is_sygus = true;
+ if (options::sygusInference() || options::sygusRewSynthInput()
+ || options::sygusAbduct())
+ {
+ d_logic = d_logic.getUnlockedCopy();
+ // sygus requires arithmetic, datatypes and quantifiers
+ d_logic.enableTheory(THEORY_ARITH);
+ d_logic.enableTheory(THEORY_DATATYPES);
+ d_logic.enableTheory(THEORY_QUANTIFIERS);
+ d_logic.lock();
+ // since we are trying to recast as sygus, we assume the input is sygus
+ is_sygus = true;
+ }
}
if ((options::checkModels() || options::checkSynthSol()
options::sygusExtRew.set(false);
}
}
+ if (options::sygusAbduct())
+ {
+ // if doing abduction, we should filter strong solutions
+ if (!options::sygusFilterSolMode.wasSetByUser())
+ {
+ options::sygusFilterSolMode.set(quantifiers::SYGUS_FILTER_SOL_STRONG);
+ }
+ }
if (options::sygusRewSynth() || options::sygusRewVerify()
- || options::sygusQueryGen())
+ || options::sygusQueryGen() || options::sygusAbduct())
{
// rewrite rule synthesis implies that sygus stream must be true
options::sygusStream.set(true);
if (options::sygusStream())
{
// Streaming is incompatible with techniques that focus the search towards
- // finding a single solution. This currently includes the PBE solver and
- // static template inference for invariant synthesis.
+ // finding a single solution. This currently includes the PBE solver,
+ // static template inference for invariant synthesis, and single
+ // invocation techniques.
if (!options::sygusUnifPbe.wasSetByUser())
{
options::sygusUnifPbe.set(false);
{
options::sygusInvTemplMode.set(quantifiers::SYGUS_INV_TEMPL_MODE_NONE);
}
+ if (!options::cegqiSingleInvMode.wasSetByUser())
+ {
+ options::cegqiSingleInvMode.set(quantifiers::CEGQI_SI_MODE_NONE);
+ }
}
//do not allow partial functions
if( !options::bitvectorDivByZeroConst.wasSetByUser() ){
"--sygus-expr-miner-check-timeout=N requires "
"--sygus-expr-miner-check-use-export");
}
- if (options::sygusRewSynthInput())
+ if (options::sygusRewSynthInput() || options::sygusAbduct())
{
- throw OptionException(
- "--sygus-rr-synth-input requires "
- "--sygus-expr-miner-check-use-export");
+ std::stringstream ss;
+ ss << (options::sygusRewSynthInput() ? "--sygus-rr-synth-input"
+ : "--sygus-abduct");
+ ss << "requires --sygus-expr-miner-check-use-export";
+ throw OptionException(ss.str());
}
}
d_smt.d_fmfRecFunctionsDefined->push_back( f );
}
}
- if (options::sygusInference())
- {
- d_passes["sygus-infer"]->apply(&d_assertions);
- }
}
if( options::sortInference() || options::ufssFairnessMonotone() ){
d_passes["pseudo-boolean-processor"]->apply(&d_assertions);
}
- if (options::sygusRewSynthInput())
+ // rephrasing normal inputs as sygus problems
+ if (!d_smt.d_isInternalSubsolver)
{
- // do candidate rewrite rule synthesis
- d_passes["synth-rr"]->apply(&d_assertions);
+ if (options::sygusInference())
+ {
+ d_passes["sygus-infer"]->apply(&d_assertions);
+ }
+ else if (options::sygusAbduct())
+ {
+ d_passes["sygus-abduct"]->apply(&d_assertions);
+ }
+ else if (options::sygusRewSynthInput())
+ {
+ // do candidate rewrite rule synthesis
+ d_passes["synth-rr"]->apply(&d_assertions);
+ }
}
Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-simplify" << endl;
nodeManagerOptions.setOption(key, optionarg);
}
+void SmtEngine::setIsInternalSubsolver() { d_isInternalSubsolver = true; }
CVC4::SExpr SmtEngine::getOption(const std::string& key) const
{
NodeManagerScope nms(d_nodeManager);
*/
Options d_originalOptions;
+ /** whether this is an internal subsolver */
+ bool d_isInternalSubsolver;
+
/**
* Number of internal pops that have been deferred.
*/
void setOption(const std::string& key, const CVC4::SExpr& value)
/* throw(OptionException, ModalException) */;
+ /** Set is internal subsolver.
+ *
+ * This function is called on SmtEngine objects that are created internally.
+ * It is used to mark that this SmtEngine should not perform preprocessing
+ * passes that rephrase the input, such as --sygus-rr-synth-input or
+ * --sygus-abduct.
+ */
+ void setIsInternalSubsolver();
+
/** sets the input name */
void setFilename(std::string filename);
/** return the input name (if any) */
try
{
checker.reset(new SmtEngine(&em));
+ checker->setIsInternalSubsolver();
checker->setTimeLimit(options::sygusExprMinerCheckTimeout(), true);
checker->setLogic(smt::currentSmtEngine()->getLogicInfo());
checker->setOption("sygus-rr-synth-input", false);
+ checker->setOption("sygus-abduct", false);
checker->setOption("input-language", "smt2");
Expr equery = squery.toExpr().exportTo(&em, varMap);
checker->assertFormula(equery);
try
{
checker.reset(new SmtEngine(&em));
+ checker->setIsInternalSubsolver();
checker->setTimeLimit(options::sygusRepairConstTimeout(), true);
checker->setLogic(smt::currentSmtEngine()->getLogicInfo());
// renable options disabled by sygus
Trace("cegqi-engine") << "Check side condition..." << std::endl;
Trace("cegqi-debug") << "Check side condition : " << sc << std::endl;
SmtEngine scSmt(nm->toExprManager());
+ scSmt.setIsInternalSubsolver();
scSmt.setLogic(smt::currentSmtEngine()->getLogicInfo());
scSmt.assertFormula(sc.toExpr());
Result r = scSmt.checkSat();
{
Trace("cegqi-engine") << " *** Verify with subcall..." << std::endl;
SmtEngine verifySmt(nm->toExprManager());
+ verifySmt.setIsInternalSubsolver();
verifySmt.setLogic(smt::currentSmtEngine()->getLogicInfo());
verifySmt.assertFormula(query.toExpr());
Result r = verifySmt.checkSat();
{
// create new smt engine to do quantifier elimination
SmtEngine smt_qe(nm->toExprManager());
+ smt_qe.setIsInternalSubsolver();
smt_qe.setLogic(smt::currentSmtEngine()->getLogicInfo());
Trace("cegqi-qep") << "Property is non-ground single invocation, run "
"QE to obtain single invocation."
regress1/strings/type002.smt2
regress1/strings/type003.smt2
regress1/strings/username_checker_min.smt2
+ regress1/sygus-abduct-test.smt2
regress1/sygus/VC22_a.sy
regress1/sygus/abv.sy
regress1/sygus/array_search_2.sy
--- /dev/null
+; COMMAND-LINE: --sygus-abduct --sygus-abort-size=2
+; EXPECT: (error "Maximum term size (2) for enumerative SyGuS exceeded.")
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 1
+
+(set-logic QF_UFLIRA)
+(declare-fun n () Int)
+(declare-fun m () Int)
+(declare-fun x () Int)
+(declare-fun y () Int)
+
+(assert (>= n 1))
+(assert (and (<= n x)(<= x (+ n 5))))
+(assert (and (<= 1 y)(<= y m)))
+
+(check-sat-assuming ((< x y)))
projects / cvc5.git / commitdiff