From: Andrew Reynolds Date: Mon, 20 Aug 2018 17:21:37 +0000 (-0500) Subject: Make sygus inference a preprocessing pass (#2334) X-Git-Tag: cvc5-1.0.0~4758 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=991af9a7a73adaa84712e93af72980ba977b1155;p=cvc5.git Make sygus inference a preprocessing pass (#2334) --- diff --git a/src/Makefile.am b/src/Makefile.am index 5e52186b9..40aa1a5af 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -99,6 +99,8 @@ libcvc4_la_SOURCES = \ preprocessing/passes/sort_infer.h \ preprocessing/passes/static_learning.cpp \ preprocessing/passes/static_learning.h \ + preprocessing/passes/sygus_inference.cpp \ + preprocessing/passes/sygus_inference.h \ preprocessing/passes/symmetry_breaker.cpp \ preprocessing/passes/symmetry_breaker.h \ preprocessing/passes/symmetry_detect.cpp \ @@ -542,8 +544,6 @@ libcvc4_la_SOURCES = \ theory/quantifiers/sygus/sygus_unif_strat.h \ theory/quantifiers/sygus/term_database_sygus.cpp \ theory/quantifiers/sygus/term_database_sygus.h \ - theory/quantifiers/sygus_inference.cpp \ - theory/quantifiers/sygus_inference.h \ theory/quantifiers/sygus_sampler.cpp \ theory/quantifiers/sygus_sampler.h \ theory/quantifiers/term_database.cpp \ diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp new file mode 100644 index 000000000..eb8835623 --- /dev/null +++ b/src/preprocessing/passes/sygus_inference.cpp @@ -0,0 +1,321 @@ +/********************* */ +/*! \file sygus_inference.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 Sygus inference module + **/ + +#include "preprocessing/passes/sygus_inference.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" + +using namespace std; +using namespace CVC4::kind; + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +SygusInference::SygusInference(PreprocessingPassContext* preprocContext) + : PreprocessingPass(preprocContext, "sygus-infer"){}; + +PreprocessingPassResult SygusInference::applyInternal( + AssertionPipeline* assertionsToPreprocess) +{ + Trace("sygus-infer") << "Run sygus inference..." << std::endl; + std::vector funs; + std::vector sols; + // see if we can succesfully solve the input as a sygus problem + if (solveSygus(assertionsToPreprocess->ref(), funs, sols)) + { + Assert(funs.size() == sols.size()); + // if so, sygus gives us function definitions + SmtEngine* master_smte = smt::currentSmtEngine(); + for (unsigned i = 0, size = funs.size(); i < size; i++) + { + std::vector args; + Node sol = sols[i]; + // if it is a non-constant function + if (sol.getKind() == LAMBDA) + { + for (const Node& v : sol[0]) + { + args.push_back(v.toExpr()); + } + sol = sol[1]; + } + master_smte->defineFunction(funs[i].toExpr(), args, sol.toExpr()); + } + + // apply substitution to everything, should result in SAT + for (unsigned i = 0, size = assertionsToPreprocess->ref().size(); i < size; + i++) + { + Node prev = (*assertionsToPreprocess)[i]; + Node curr = + prev.substitute(funs.begin(), funs.end(), sols.begin(), sols.end()); + if (curr != prev) + { + curr = theory::Rewriter::rewrite(curr); + Trace("sygus-infer-debug") + << "...rewrote " << prev << " to " << curr << std::endl; + assertionsToPreprocess->replace(i, curr); + } + } + } + return PreprocessingPassResult::NO_CONFLICT; +} + +bool SygusInference::solveSygus(std::vector& assertions, + std::vector& funs, + std::vector& sols) +{ + if (assertions.empty()) + { + Trace("sygus-infer") << "...fail: empty assertions." << std::endl; + return false; + } + + NodeManager* nm = NodeManager::currentNM(); + + // collect free variables in all assertions + std::vector qvars; + std::map > qtvars; + std::vector free_functions; + + std::vector visit; + std::unordered_set visited; + + // add top-level conjuncts to eassertions + std::vector assertions_proc = assertions; + std::vector eassertions; + unsigned index = 0; + while (index < assertions_proc.size()) + { + Node ca = assertions_proc[index]; + if (ca.getKind() == AND) + { + for (const Node& ai : ca) + { + assertions_proc.push_back(ai); + } + } + else + { + eassertions.push_back(ca); + } + index++; + } + + // process eassertions + std::vector processed_assertions; + for (const Node& as : eassertions) + { + // substitution for this assertion + std::vector vars; + std::vector subs; + std::map type_count; + Node pas = as; + // rewrite + pas = theory::Rewriter::rewrite(pas); + Trace("sygus-infer") << "assertion : " << pas << std::endl; + if (pas.getKind() == FORALL) + { + // preprocess the quantified formula + pas = theory::quantifiers::QuantifiersRewriter::preprocess(pas); + Trace("sygus-infer-debug") << " ...preprocessed to " << pas << std::endl; + } + if (pas.getKind() == FORALL) + { + // it must be a standard quantifier + theory::quantifiers::QAttributes qa; + theory::quantifiers::QuantAttributes::computeQuantAttributes(pas, qa); + if (!qa.isStandard()) + { + Trace("sygus-infer") + << "...fail: non-standard top-level quantifier." << std::endl; + return false; + } + // infer prefix + for (const Node& v : pas[0]) + { + TypeNode tnv = v.getType(); + unsigned vnum = type_count[tnv]; + type_count[tnv]++; + if (vnum < qtvars[tnv].size()) + { + vars.push_back(v); + subs.push_back(qtvars[tnv][vnum]); + } + else + { + Assert(vnum == qtvars[tnv].size()); + qtvars[tnv].push_back(v); + qvars.push_back(v); + } + } + pas = pas[1]; + if (!vars.empty()) + { + pas = + pas.substitute(vars.begin(), vars.end(), subs.begin(), subs.end()); + } + } + Trace("sygus-infer-debug") << " ...substituted to " << pas << std::endl; + + // collect free functions, ensure no quantified formulas + TNode cur = pas; + // compute free variables + visit.push_back(cur); + do + { + cur = visit.back(); + visit.pop_back(); + if (visited.find(cur) == visited.end()) + { + visited.insert(cur); + if (cur.getKind() == APPLY_UF) + { + Node op = cur.getOperator(); + if (std::find(free_functions.begin(), free_functions.end(), op) + == free_functions.end()) + { + free_functions.push_back(op); + } + } + else if (cur.getKind() == VARIABLE) + { + // a free variable is a 0-argument function to synthesize + Assert(std::find(free_functions.begin(), free_functions.end(), cur) + == free_functions.end()); + free_functions.push_back(cur); + } + else if (cur.getKind() == FORALL) + { + Trace("sygus-infer") + << "...fail: non-top-level quantifier." << std::endl; + return false; + } + for (const TNode& cn : cur) + { + visit.push_back(cn); + } + } + } while (!visit.empty()); + processed_assertions.push_back(pas); + } + + // no functions to synthesize + if (free_functions.empty()) + { + Trace("sygus-infer") << "...fail: no free function symbols." << std::endl; + return false; + } + + Assert(!processed_assertions.empty()); + // conjunction of the assertions + Trace("sygus-infer") << "Construct body..." << std::endl; + Node body; + if (processed_assertions.size() == 1) + { + body = processed_assertions[0]; + } + else + { + body = nm->mkNode(AND, processed_assertions); + } + + // for each free function symbol, make a bound variable of the same type + Trace("sygus-infer") << "Do free function substitution..." << std::endl; + std::vector ff_vars; + std::map ff_var_to_ff; + for (const Node& ff : free_functions) + { + Node ffv = nm->mkBoundVar(ff.getType()); + ff_vars.push_back(ffv); + Trace("sygus-infer") << " synth-fun: " << ff << " as " << ffv << std::endl; + ff_var_to_ff[ffv] = ff; + } + // substitute free functions -> variables + body = body.substitute(free_functions.begin(), + free_functions.end(), + ff_vars.begin(), + ff_vars.end()); + Trace("sygus-infer-debug") << "...got : " << body << std::endl; + + // quantify the body + Trace("sygus-infer") << "Make inner sygus conjecture..." << std::endl; + if (!qvars.empty()) + { + Node bvl = nm->mkNode(BOUND_VAR_LIST, qvars); + body = nm->mkNode(EXISTS, bvl, body.negate()); + } + + // sygus attribute to mark the conjecture as a sygus conjecture + Trace("sygus-infer") << "Make outer sygus conjecture..." << std::endl; + Node sygusVar = nm->mkSkolem("sygus", nm->booleanType()); + theory::SygusAttribute ca; + sygusVar.setAttribute(ca, true); + Node instAttr = nm->mkNode(INST_ATTRIBUTE, sygusVar); + Node instAttrList = nm->mkNode(INST_PATTERN_LIST, instAttr); + + Node fbvl = nm->mkNode(BOUND_VAR_LIST, ff_vars); + + body = nm->mkNode(FORALL, fbvl, body, instAttrList); + + Trace("sygus-infer") << "*** Return sygus inference : " << body << std::endl; + + // make a separate smt call + SmtEngine rrSygus(nm->toExprManager()); + rrSygus.setLogic(smt::currentSmtEngine()->getLogicInfo()); + rrSygus.assertFormula(body.toExpr()); + Trace("sygus-infer") << "*** Check sat..." << std::endl; + Result r = rrSygus.checkSat(); + Trace("sygus-infer") << "...result : " << r << std::endl; + if (r.asSatisfiabilityResult().isSat() != Result::UNSAT) + { + // failed, conjecture was infeasible + return false; + } + // get the synthesis solutions + std::map synth_sols; + rrSygus.getSynthSolutions(synth_sols); + + std::vector final_ff; + std::vector final_ff_sol; + for (std::map::iterator it = synth_sols.begin(); + it != synth_sols.end(); + ++it) + { + Trace("sygus-infer") << " synth sol : " << it->first << " -> " + << it->second << std::endl; + Node ffv = Node::fromExpr(it->first); + std::map::iterator itffv = ff_var_to_ff.find(ffv); + // all synthesis solutions should correspond to a variable we introduced + Assert(itffv != ff_var_to_ff.end()); + if (itffv != ff_var_to_ff.end()) + { + Node ff = itffv->second; + Node body = Node::fromExpr(it->second); + Trace("sygus-infer") << "Define " << ff << " as " << body << std::endl; + funs.push_back(ff); + sols.push_back(body); + } + } + return true; +} + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 diff --git a/src/preprocessing/passes/sygus_inference.h b/src/preprocessing/passes/sygus_inference.h new file mode 100644 index 000000000..5e7c6f7d0 --- /dev/null +++ b/src/preprocessing/passes/sygus_inference.h @@ -0,0 +1,71 @@ +/********************* */ +/*! \file sygus_inference.h + ** \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 SygusInference + **/ + +#ifndef __CVC4__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_ +#define __CVC4__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_ + +#include +#include +#include +#include "expr/node.h" + +#include "preprocessing/preprocessing_pass.h" +#include "preprocessing/preprocessing_pass_context.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +/** SygusInference + * + * A preprocessing utility that turns a set of (quantified) assertions into a + * single SyGuS conjecture. If this is possible, we solve for this single Sygus + * conjecture using a separate copy of the SMT engine. If sygus successfully + * solves the conjecture, we plug the synthesis solutions back into the original + * problem, thus obtaining a set of model substitutions under which the + * assertions should simplify to true. + */ +class SygusInference : public PreprocessingPass +{ + public: + SygusInference(PreprocessingPassContext* preprocContext); + + protected: + /** + * Either replaces all uninterpreted functions in assertions by their + * interpretation in a sygus solution, or leaves the assertions unmodified. + */ + PreprocessingPassResult applyInternal( + AssertionPipeline* assertionsToPreprocess) override; + /** solve sygus + * + * Returns true if we can recast the input problem assertions as a sygus + * problem and successfully solve it using a separate call to an SMT engine. + * + * We fail if either a sygus conjecture that corresponds to assertions cannot + * be inferred, or the sygus conjecture we infer is infeasible. + * + * If this function returns true, then we add all uninterpreted symbols s in + * assertions to funs and their corresponding solution to sols. + */ + bool solveSygus(std::vector& assertions, + std::vector& funs, + std::vector& sols); +}; + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 + +#endif /* __CVC4__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_ */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 418028d09..1e8ae4033 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -88,6 +88,7 @@ #include "preprocessing/passes/sep_skolem_emp.h" #include "preprocessing/passes/sort_infer.h" #include "preprocessing/passes/static_learning.h" +#include "preprocessing/passes/sygus_inference.h" #include "preprocessing/passes/symmetry_breaker.h" #include "preprocessing/passes/symmetry_detect.h" #include "preprocessing/passes/synth_rew_rules.h" @@ -119,7 +120,6 @@ #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/single_inv_partition.h" #include "theory/quantifiers/sygus/ce_guided_instantiation.h" -#include "theory/quantifiers/sygus_inference.h" #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" #include "theory/sort_inference.h" @@ -2676,6 +2676,8 @@ void SmtEnginePrivate::finishInit() d_smt.d_theoryEngine->getSortInference())); std::unique_ptr staticLearning( new StaticLearning(d_preprocessingPassContext.get())); + std::unique_ptr sygusInfer( + new SygusInference(d_preprocessingPassContext.get())); std::unique_ptr sbProc( new SymBreakerPass(d_preprocessingPassContext.get())); std::unique_ptr srrProc( @@ -2713,6 +2715,8 @@ void SmtEnginePrivate::finishInit() std::move(sortInfer)); d_preprocessingPassRegistry.registerPass("static-learning", std::move(staticLearning)); + d_preprocessingPassRegistry.registerPass("sygus-infer", + std::move(sygusInfer)); d_preprocessingPassRegistry.registerPass("sym-break", std::move(sbProc)); d_preprocessingPassRegistry.registerPass("synth-rr", std::move(srrProc)); } @@ -4243,12 +4247,7 @@ void SmtEnginePrivate::processAssertions() { } if (options::sygusInference()) { - // try recast as sygus - quantifiers::SygusInference si; - if (si.simplify(d_assertions.ref())) - { - Trace("smt-proc") << "...converted to sygus conjecture." << std::endl; - } + d_preprocessingPassRegistry.getPass("sygus-infer")->apply(&d_assertions); } Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-quant-preprocess" << endl; } diff --git a/src/theory/quantifiers/sygus_inference.cpp b/src/theory/quantifiers/sygus_inference.cpp deleted file mode 100644 index 6232de6fe..000000000 --- a/src/theory/quantifiers/sygus_inference.cpp +++ /dev/null @@ -1,302 +0,0 @@ -/********************* */ -/*! \file sygus_inference.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_inference - **/ - -#include "theory/quantifiers/sygus_inference.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" - -using namespace CVC4::kind; - -namespace CVC4 { -namespace theory { -namespace quantifiers { - -SygusInference::SygusInference() {} - -bool SygusInference::simplify(std::vector& assertions) -{ - Trace("sygus-infer") << "Run sygus inference..." << std::endl; - - if (assertions.empty()) - { - Trace("sygus-infer") << "...fail: empty assertions." << std::endl; - return false; - } - - NodeManager* nm = NodeManager::currentNM(); - - // collect free variables in all assertions - std::vector qvars; - std::map > qtvars; - std::vector free_functions; - - std::vector visit; - std::unordered_set visited; - - // add top-level conjuncts to eassertions - std::vector assertions_proc = assertions; - std::vector eassertions; - unsigned index = 0; - while (index < assertions_proc.size()) - { - Node ca = assertions_proc[index]; - if (ca.getKind() == AND) - { - for (const Node& ai : ca) - { - assertions_proc.push_back(ai); - } - } - else - { - eassertions.push_back(ca); - } - index++; - } - - // process eassertions - std::vector processed_assertions; - for (const Node& as : eassertions) - { - // substitution for this assertion - std::vector vars; - std::vector subs; - std::map type_count; - Node pas = as; - // rewrite - pas = Rewriter::rewrite(pas); - Trace("sygus-infer") << "assertion : " << pas << std::endl; - if (pas.getKind() == FORALL) - { - // preprocess the quantified formula - pas = quantifiers::QuantifiersRewriter::preprocess(pas); - Trace("sygus-infer-debug") << " ...preprocessed to " << pas << std::endl; - } - if (pas.getKind() == FORALL) - { - // it must be a standard quantifier - QAttributes qa; - QuantAttributes::computeQuantAttributes(pas, qa); - if (!qa.isStandard()) - { - Trace("sygus-infer") - << "...fail: non-standard top-level quantifier." << std::endl; - return false; - } - // infer prefix - for (const Node& v : pas[0]) - { - TypeNode tnv = v.getType(); - unsigned vnum = type_count[tnv]; - type_count[tnv]++; - if (vnum < qtvars[tnv].size()) - { - vars.push_back(v); - subs.push_back(qtvars[tnv][vnum]); - } - else - { - Assert(vnum == qtvars[tnv].size()); - qtvars[tnv].push_back(v); - qvars.push_back(v); - } - } - pas = pas[1]; - if (!vars.empty()) - { - pas = - pas.substitute(vars.begin(), vars.end(), subs.begin(), subs.end()); - } - } - Trace("sygus-infer-debug") << " ...substituted to " << pas << std::endl; - - // collect free functions, ensure no quantified formulas - TNode cur = pas; - // compute free variables - visit.push_back(cur); - do - { - cur = visit.back(); - visit.pop_back(); - if (visited.find(cur) == visited.end()) - { - visited.insert(cur); - if (cur.getKind() == APPLY_UF) - { - Node op = cur.getOperator(); - if (std::find(free_functions.begin(), free_functions.end(), op) - == free_functions.end()) - { - free_functions.push_back(op); - } - } - else if (cur.getKind() == VARIABLE) - { - // a free variable is a 0-argument function to synthesize - Assert(std::find(free_functions.begin(), free_functions.end(), cur) - == free_functions.end()); - free_functions.push_back(cur); - } - else if (cur.getKind() == FORALL) - { - Trace("sygus-infer") - << "...fail: non-top-level quantifier." << std::endl; - return false; - } - for (const TNode& cn : cur) - { - visit.push_back(cn); - } - } - } while (!visit.empty()); - processed_assertions.push_back(pas); - } - - // no functions to synthesize - if (free_functions.empty()) - { - Trace("sygus-infer") << "...fail: no free function symbols." << std::endl; - return false; - } - - Assert(!processed_assertions.empty()); - // conjunction of the assertions - Trace("sygus-infer") << "Construct body..." << std::endl; - Node body; - if (processed_assertions.size() == 1) - { - body = processed_assertions[0]; - } - else - { - body = nm->mkNode(AND, processed_assertions); - } - - // for each free function symbol, make a bound variable of the same type - Trace("sygus-infer") << "Do free function substitution..." << std::endl; - std::vector ff_vars; - std::map ff_var_to_ff; - for (const Node& ff : free_functions) - { - Node ffv = nm->mkBoundVar(ff.getType()); - ff_vars.push_back(ffv); - Trace("sygus-infer") << " synth-fun: " << ff << " as " << ffv << std::endl; - ff_var_to_ff[ffv] = ff; - } - // substitute free functions -> variables - body = body.substitute(free_functions.begin(), - free_functions.end(), - ff_vars.begin(), - ff_vars.end()); - Trace("sygus-infer-debug") << "...got : " << body << std::endl; - - // quantify the body - Trace("sygus-infer") << "Make inner sygus conjecture..." << std::endl; - if (!qvars.empty()) - { - Node bvl = nm->mkNode(BOUND_VAR_LIST, qvars); - body = nm->mkNode(EXISTS, bvl, body.negate()); - } - - // sygus attribute to mark the conjecture as a sygus conjecture - Trace("sygus-infer") << "Make outer sygus conjecture..." << std::endl; - Node sygusVar = nm->mkSkolem("sygus", nm->booleanType()); - SygusAttribute ca; - sygusVar.setAttribute(ca, true); - Node instAttr = nm->mkNode(INST_ATTRIBUTE, sygusVar); - Node instAttrList = nm->mkNode(INST_PATTERN_LIST, instAttr); - - Node fbvl = nm->mkNode(BOUND_VAR_LIST, ff_vars); - - body = nm->mkNode(FORALL, fbvl, body, instAttrList); - - Trace("sygus-infer") << "*** Return sygus inference : " << body << std::endl; - - // make a separate smt call - SmtEngine* master_smte = smt::currentSmtEngine(); - SmtEngine rrSygus(nm->toExprManager()); - rrSygus.setLogic(smt::currentSmtEngine()->getLogicInfo()); - rrSygus.assertFormula(body.toExpr()); - Trace("sygus-infer") << "*** Check sat..." << std::endl; - Result r = rrSygus.checkSat(); - Trace("sygus-infer") << "...result : " << r << std::endl; - if (r.asSatisfiabilityResult().isSat() != Result::UNSAT) - { - // failed, conjecture was infeasible - return false; - } - // get the synthesis solutions - std::map synth_sols; - rrSygus.getSynthSolutions(synth_sols); - - std::vector final_ff; - std::vector final_ff_sol; - for (std::map::iterator it = synth_sols.begin(); - it != synth_sols.end(); - ++it) - { - Node lambda = Node::fromExpr(it->second); - Trace("sygus-infer") << " synth sol : " << it->first << " -> " - << it->second << std::endl; - Node ffv = Node::fromExpr(it->first); - std::map::iterator itffv = ff_var_to_ff.find(ffv); - // all synthesis solutions should correspond to a variable we introduced - Assert(itffv != ff_var_to_ff.end()); - if (itffv != ff_var_to_ff.end()) - { - Node ff = itffv->second; - Expr body = it->second; - std::vector args; - // if it is a non-constant function - if (lambda.getKind() == LAMBDA) - { - for (const Node& v : lambda[0]) - { - args.push_back(v.toExpr()); - } - body = it->second[1]; - } - Trace("sygus-infer") << "Define " << ff << " as " << it->second - << std::endl; - final_ff.push_back(ff); - final_ff_sol.push_back(it->second); - master_smte->defineFunction(ff.toExpr(), args, body); - } - } - - // apply substitution to everything, should result in SAT - for (unsigned i = 0, size = assertions.size(); i < size; i++) - { - Node prev = assertions[i]; - Node curr = assertions[i].substitute(final_ff.begin(), - final_ff.end(), - final_ff_sol.begin(), - final_ff_sol.end()); - if (curr != prev) - { - curr = Rewriter::rewrite(curr); - Trace("sygus-infer-debug") - << "...rewrote " << prev << " to " << curr << std::endl; - assertions[i] = curr; - } - } - return true; -} - -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ diff --git a/src/theory/quantifiers/sygus_inference.h b/src/theory/quantifiers/sygus_inference.h deleted file mode 100644 index 414103fc7..000000000 --- a/src/theory/quantifiers/sygus_inference.h +++ /dev/null @@ -1,57 +0,0 @@ -/********************* */ -/*! \file sygus_inference.h - ** \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 sygus_inference - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_INFERENCE_H -#define __CVC4__THEORY__QUANTIFIERS__SYGUS_INFERENCE_H - -#include -#include "expr/node.h" - -namespace CVC4 { -namespace theory { -namespace quantifiers { - -/** SygusInference - * - * A preprocessing utility that turns a set of (quantified) assertions into a - * single SyGuS conjecture. If this is possible, we solve for this single Sygus - * conjecture using a separate copy of the SMT engine. If sygus successfully - * solves the conjecture, we plug the synthesis solutions back into the original - * problem, thus obtaining a set of model substitutions under which the - * assertions should simplify to true. - */ -class SygusInference -{ - public: - SygusInference(); - ~SygusInference() {} - /** simplify assertions - * - * Either replaces all uninterpreted functions in assertions by their - * interpretation in the solution found by a separate call to an SMT engine - * and returns true, or leaves the assertions unmodified and returns false. - * - * We fail if either a sygus conjecture that corresponds to assertions cannot - * be inferred, or the sygus conjecture we infer is infeasible. - */ - bool simplify(std::vector& assertions); -}; - -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ - -#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_INFERENCE_H */