diff options
| -rw-r--r-- | src/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | src/options/quantifiers_options.toml | 10 | ||||
| -rw-r--r-- | src/preprocessing/passes/sygus_abduct.cpp | 174 | ||||
| -rw-r--r-- | src/preprocessing/passes/sygus_abduct.h | 72 | ||||
| -rw-r--r-- | src/preprocessing/preprocessing_pass_registry.cpp | 2 | ||||
| -rw-r--r-- | src/smt/smt_engine.cpp | 75 | ||||
| -rw-r--r-- | src/smt/smt_engine.h | 12 | ||||
| -rw-r--r-- | src/theory/quantifiers/expr_miner.cpp | 2 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_repair_const.cpp | 1 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.cpp | 2 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/synth_engine.cpp | 1 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/sygus-abduct-test.smt2 | 16 |
13 files changed, 347 insertions, 23 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 5f34fe59b..244845fda 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -88,6 +88,8 @@ libcvc4_add_sources( 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 diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 4deb5565d..1ff85c96d 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -877,6 +877,15 @@ header = "options/quantifiers_options.h" 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" long = "cegqi" @@ -1428,6 +1437,7 @@ header = "options/quantifiers_options.h" default = "false" help = "compute backwards filtering to compute whether previous solutions are filtered based on later ones" + [[option]] name = "sygusExprMinerCheckUseExport" category = "expert" diff --git a/src/preprocessing/passes/sygus_abduct.cpp b/src/preprocessing/passes/sygus_abduct.cpp new file mode 100644 index 000000000..a2fe38219 --- /dev/null +++ b/src/preprocessing/passes/sygus_abduct.cpp @@ -0,0 +1,174 @@ +/********************* */ +/*! \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 diff --git a/src/preprocessing/passes/sygus_abduct.h b/src/preprocessing/passes/sygus_abduct.h new file mode 100644 index 000000000..8e83bf1d7 --- /dev/null +++ b/src/preprocessing/passes/sygus_abduct.h @@ -0,0 +1,72 @@ +/********************* */ +/*! \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_ */ diff --git a/src/preprocessing/preprocessing_pass_registry.cpp b/src/preprocessing/preprocessing_pass_registry.cpp index f2e7c8603..30bbf41c9 100644 --- a/src/preprocessing/preprocessing_pass_registry.cpp +++ b/src/preprocessing/preprocessing_pass_registry.cpp @@ -48,6 +48,7 @@ #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" @@ -126,6 +127,7 @@ PreprocessingPassRegistry::PreprocessingPassRegistry() 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>); diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 8427599a9..8305d1d4d 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -879,6 +879,7 @@ SmtEngine::SmtEngine(ExprManager* em) d_defineCommands(), d_logic(), d_originalOptions(), + d_isInternalSubsolver(false), d_pendingPops(0), d_fullyInited(false), d_problemExtended(false), @@ -1264,16 +1265,20 @@ void SmtEngine::setDefaults() { } // 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() @@ -1958,8 +1963,16 @@ void SmtEngine::setDefaults() { 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); @@ -1967,8 +1980,9 @@ void SmtEngine::setDefaults() { 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); @@ -1982,6 +1996,10 @@ void SmtEngine::setDefaults() { { 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() ){ @@ -2282,11 +2300,13 @@ void SmtEngine::setDefaults() { "--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()); } } @@ -3314,10 +3334,6 @@ void SmtEnginePrivate::processAssertions() { d_smt.d_fmfRecFunctionsDefined->push_back( f ); } } - if (options::sygusInference()) - { - d_passes["sygus-infer"]->apply(&d_assertions); - } } if( options::sortInference() || options::ufssFairnessMonotone() ){ @@ -3328,10 +3344,22 @@ void SmtEnginePrivate::processAssertions() { 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; @@ -5297,6 +5325,7 @@ void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value) nodeManagerOptions.setOption(key, optionarg); } +void SmtEngine::setIsInternalSubsolver() { d_isInternalSubsolver = true; } CVC4::SExpr SmtEngine::getOption(const std::string& key) const { NodeManagerScope nms(d_nodeManager); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index e53d1eb55..5c41feaba 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -209,6 +209,9 @@ class CVC4_PUBLIC SmtEngine { */ Options d_originalOptions; + /** whether this is an internal subsolver */ + bool d_isInternalSubsolver; + /** * Number of internal pops that have been deferred. */ @@ -502,6 +505,15 @@ class CVC4_PUBLIC SmtEngine { 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) */ diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp index b65d1c522..65678f674 100644 --- a/src/theory/quantifiers/expr_miner.cpp +++ b/src/theory/quantifiers/expr_miner.cpp @@ -87,9 +87,11 @@ void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker, 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); diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index 09525712f..18722a192 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -115,6 +115,7 @@ void SygusRepairConst::initializeChecker(std::unique_ptr<SmtEngine>& checker, try { checker.reset(new SmtEngine(&em)); + checker->setIsInternalSubsolver(); checker->setTimeLimit(options::sygusRepairConstTimeout(), true); checker->setLogic(smt::currentSmtEngine()->getLogicInfo()); // renable options disabled by sygus diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index e25e8a225..2e0fa75fe 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -540,6 +540,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems) 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(); @@ -572,6 +573,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems) { 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(); diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index d3eff1750..0623c257a 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -159,6 +159,7 @@ void SynthEngine::assignConjecture(Node q) { // 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." diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 0b4a4bdc7..21e08f2bf 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1582,6 +1582,7 @@ set(regress_1_tests 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 diff --git a/test/regress/regress1/sygus-abduct-test.smt2 b/test/regress/regress1/sygus-abduct-test.smt2 new file mode 100644 index 000000000..4ac90870c --- /dev/null +++ b/test/regress/regress1/sygus-abduct-test.smt2 @@ -0,0 +1,16 @@ +; 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))) |