summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/CMakeLists.txt4
-rw-r--r--src/bindings/java/CMakeLists.txt1
-rw-r--r--src/options/quantifiers_options.toml9
-rw-r--r--src/options/smt_options.toml9
-rw-r--r--src/parser/smt2/Smt2.g16
-rw-r--r--src/parser/smt2/smt2.cpp7
-rw-r--r--src/preprocessing/preprocessing_pass_registry.cpp2
-rw-r--r--src/smt/command.cpp84
-rw-r--r--src/smt/command.h50
-rw-r--r--src/smt/smt_engine.cpp140
-rw-r--r--src/smt/smt_engine.h43
-rw-r--r--src/theory/logic_info.cpp9
-rw-r--r--src/theory/logic_info.h6
-rw-r--r--src/theory/quantifiers/expr_miner.cpp1
-rw-r--r--src/theory/quantifiers/sygus/sygus_abduct.cpp (renamed from src/preprocessing/passes/sygus_abduct.cpp)73
-rw-r--r--src/theory/quantifiers/sygus/sygus_abduct.h (renamed from src/preprocessing/passes/sygus_abduct.h)54
16 files changed, 384 insertions, 124 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 9da9bd603..861841633 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -90,8 +90,6 @@ 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
@@ -551,6 +549,8 @@ libcvc4_add_sources(
theory/quantifiers/sygus/cegis_unif.h
theory/quantifiers/sygus/enum_stream_substitution.cpp
theory/quantifiers/sygus/enum_stream_substitution.h
+ theory/quantifiers/sygus/sygus_abduct.cpp
+ theory/quantifiers/sygus/sygus_abduct.h
theory/quantifiers/sygus/sygus_enumerator.cpp
theory/quantifiers/sygus/sygus_enumerator.h
theory/quantifiers/sygus/sygus_eval_unfold.cpp
diff --git a/src/bindings/java/CMakeLists.txt b/src/bindings/java/CMakeLists.txt
index a94afc0a0..555ab2d6f 100644
--- a/src/bindings/java/CMakeLists.txt
+++ b/src/bindings/java/CMakeLists.txt
@@ -111,6 +111,7 @@ set(gen_java_files
${CMAKE_CURRENT_BINARY_DIR}/FloatingPointToUBV.java
${CMAKE_CURRENT_BINARY_DIR}/FloatingPointType.java
${CMAKE_CURRENT_BINARY_DIR}/FunctionType.java
+ ${CMAKE_CURRENT_BINARY_DIR}/GetAbductCommand.java
${CMAKE_CURRENT_BINARY_DIR}/GetAssertionsCommand.java
${CMAKE_CURRENT_BINARY_DIR}/GetAssignmentCommand.java
${CMAKE_CURRENT_BINARY_DIR}/GetInfoCommand.java
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 03ffade46..8792fb56b 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -886,15 +886,6 @@ 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"
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 72dfdd7f8..ef4e19654 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -614,3 +614,12 @@ header = "options/smt_options.h"
default = "false"
read_only = true
help = "attempt to solve a pure real satisfiable problem as an integer problem (for non-linear)"
+
+[[option]]
+ name = "produceAbducts"
+ category = "undocumented"
+ long = "produce-abducts"
+ type = "bool"
+ default = "false"
+ read_only = true
+ help = "support the get-abduct command"
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index d72188c6c..a95689f1c 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1529,8 +1529,19 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
| GET_QE_DISJUNCT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
term[e,e2]
{ cmd->reset(new GetQuantifierEliminationCommand(e, false)); }
- | DECLARE_HEAP LPAREN_TOK
- sortSymbol[t,CHECK_DECLARED]
+ | GET_ABDUCT_TOK {
+ PARSER_STATE->checkThatLogicIsSet();
+ }
+ symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
+ term[e,e2]
+ (
+ sygusGrammar[t, terms, name]
+ )?
+ {
+ cmd->reset(new GetAbductCommand(name,e, t));
+ }
+ | DECLARE_HEAP LPAREN_TOK
+ sortSymbol[t,CHECK_DECLARED]
sortSymbol[t, CHECK_DECLARED]
// We currently do nothing with the type information declared for the heap.
{ cmd->reset(new EmptyCommand()); }
@@ -3055,6 +3066,7 @@ SIMPLIFY_TOK : 'simplify';
INCLUDE_TOK : 'include';
GET_QE_TOK : 'get-qe';
GET_QE_DISJUNCT_TOK : 'get-qe-disjunct';
+GET_ABDUCT_TOK : 'get-abduct';
DECLARE_HEAP : 'declare-heap';
// SyGuS commands
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 278f2bdfd..752bf58b4 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -674,11 +674,8 @@ Command* Smt2::setLogic(std::string name, bool fromCommand)
}
// get unlocked copy, modify, copy and relock
LogicInfo log(d_logic.getUnlockedCopy());
- log.enableQuantifiers();
- log.enableTheory(theory::THEORY_UF);
- log.enableTheory(theory::THEORY_DATATYPES);
- log.enableIntegers();
- log.enableHigherOrder();
+ // enable everything needed for sygus
+ log.enableSygus();
d_logic = log;
d_logic.lock();
}
diff --git a/src/preprocessing/preprocessing_pass_registry.cpp b/src/preprocessing/preprocessing_pass_registry.cpp
index 15618f575..34bae1224 100644
--- a/src/preprocessing/preprocessing_pass_registry.cpp
+++ b/src/preprocessing/preprocessing_pass_registry.cpp
@@ -48,7 +48,6 @@
#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"
@@ -127,7 +126,6 @@ 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/command.cpp b/src/smt/command.cpp
index b1936d8cc..044062f77 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -2033,6 +2033,90 @@ std::string GetSynthSolutionCommand::getCommandName() const
return "get-instantiations";
}
+GetAbductCommand::GetAbductCommand() {}
+GetAbductCommand::GetAbductCommand(const std::string& name, Expr conj)
+ : d_name(name), d_conj(conj), d_resultStatus(false)
+{
+}
+GetAbductCommand::GetAbductCommand(const std::string& name,
+ Expr conj,
+ const Type& gtype)
+ : d_name(name),
+ d_conj(conj),
+ d_sygus_grammar_type(gtype),
+ d_resultStatus(false)
+{
+}
+
+Expr GetAbductCommand::getConjecture() const { return d_conj; }
+Type GetAbductCommand::getGrammarType() const { return d_sygus_grammar_type; }
+Expr GetAbductCommand::getResult() const { return d_result; }
+
+void GetAbductCommand::invoke(SmtEngine* smtEngine)
+{
+ try
+ {
+ if (d_sygus_grammar_type.isNull())
+ {
+ d_resultStatus = smtEngine->getAbduct(d_conj, d_result);
+ }
+ else
+ {
+ d_resultStatus =
+ smtEngine->getAbduct(d_conj, d_sygus_grammar_type, d_result);
+ }
+ d_commandStatus = CommandSuccess::instance();
+ }
+ catch (exception& e)
+ {
+ d_commandStatus = new CommandFailure(e.what());
+ }
+}
+
+void GetAbductCommand::printResult(std::ostream& out, uint32_t verbosity) const
+{
+ if (!ok())
+ {
+ this->Command::printResult(out, verbosity);
+ }
+ else
+ {
+ expr::ExprDag::Scope scope(out, false);
+ if (d_resultStatus)
+ {
+ out << "(define-fun " << d_name << " () Bool " << d_result << ")"
+ << std::endl;
+ }
+ else
+ {
+ out << "none" << std::endl;
+ }
+ }
+}
+
+Command* GetAbductCommand::exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap)
+{
+ GetAbductCommand* c =
+ new GetAbductCommand(d_name, d_conj.exportTo(exprManager, variableMap));
+ c->d_sygus_grammar_type =
+ d_sygus_grammar_type.exportTo(exprManager, variableMap);
+ c->d_result = d_result.exportTo(exprManager, variableMap);
+ c->d_resultStatus = d_resultStatus;
+ return c;
+}
+
+Command* GetAbductCommand::clone() const
+{
+ GetAbductCommand* c = new GetAbductCommand(d_name, d_conj);
+ c->d_sygus_grammar_type = d_sygus_grammar_type;
+ c->d_result = d_result;
+ c->d_resultStatus = d_resultStatus;
+ return c;
+}
+
+std::string GetAbductCommand::getCommandName() const { return "get-abduct"; }
+
/* -------------------------------------------------------------------------- */
/* class GetQuantifierEliminationCommand */
/* -------------------------------------------------------------------------- */
diff --git a/src/smt/command.h b/src/smt/command.h
index 68f9d1881..eb3199944 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -1009,6 +1009,56 @@ class CVC4_PUBLIC GetSynthSolutionCommand : public Command
SmtEngine* d_smtEngine;
}; /* class GetSynthSolutionCommand */
+/** The command (get-abduct s B (G)?)
+ *
+ * This command asks for an abduct from the current set of assertions and
+ * conjecture (goal) given by the argument B.
+ *
+ * The symbol s is the name for the abduction predicate. If we successfully
+ * find a predicate P, then the output response of this command is:
+ * (define-fun s () Bool P)
+ *
+ * A grammar type G can be optionally provided to indicate the syntactic
+ * restrictions on the possible solutions returned.
+ */
+class CVC4_PUBLIC GetAbductCommand : public Command
+{
+ public:
+ GetAbductCommand();
+ GetAbductCommand(const std::string& name, Expr conj);
+ GetAbductCommand(const std::string& name, Expr conj, const Type& gtype);
+
+ /** Get the conjecture of the abduction query */
+ Expr getConjecture() const;
+ /** Get the grammar type given for the abduction query */
+ Type getGrammarType() const;
+ /** Get the result of the query, which is the solution to the abduction query.
+ */
+ Expr getResult() const;
+
+ void invoke(SmtEngine* smtEngine) override;
+ void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
+ Command* exportTo(ExprManager* exprManager,
+ ExprManagerMapCollection& variableMap) override;
+ Command* clone() const override;
+ std::string getCommandName() const override;
+
+ protected:
+ /** The name of the abduction predicate */
+ std::string d_name;
+ /** The conjecture of the abduction query */
+ Expr d_conj;
+ /**
+ * The (optional) grammar of the abduction query, expressed as a sygus
+ * datatype type.
+ */
+ Type d_sygus_grammar_type;
+ /** the return status of the command */
+ bool d_resultStatus;
+ /** the return expression of the command */
+ Expr d_result;
+}; /* class GetAbductCommand */
+
class CVC4_PUBLIC GetQuantifierEliminationCommand : public Command
{
protected:
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 5e8540348..5db3fc43d 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -98,6 +98,7 @@
#include "theory/quantifiers/fun_def_process.h"
#include "theory/quantifiers/quantifiers_rewriter.h"
#include "theory/quantifiers/single_inv_partition.h"
+#include "theory/quantifiers/sygus/sygus_abduct.h"
#include "theory/quantifiers/sygus/synth_engine.h"
#include "theory/quantifiers/term_util.h"
#include "theory/rewriter.h"
@@ -1258,21 +1259,25 @@ void SmtEngine::setDefaults() {
// sygus inference may require datatypes
if (!d_isInternalSubsolver)
{
- if (options::sygusInference() || options::sygusRewSynthInput()
- || options::sygusAbduct())
+ if (options::produceAbducts())
+ {
+ // we may invoke a sygus conjecture, hence we need options related to
+ // sygus
+ is_sygus = true;
+ }
+ if (options::sygusInference() || options::sygusRewSynthInput())
{
- 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;
+ // we change the logic to incorporate sygus immediately
+ d_logic = d_logic.getUnlockedCopy();
+ d_logic.enableSygus();
+ d_logic.lock();
}
}
if ((options::checkModels() || options::checkSynthSol()
+ || options::produceAbducts()
|| options::modelCoresMode() != MODEL_CORES_NONE)
&& !options::produceAssertions())
{
@@ -1954,16 +1959,24 @@ void SmtEngine::setDefaults() {
options::sygusExtRew.set(false);
}
}
- if (options::sygusAbduct())
+ // Whether we must use "basic" sygus algorithms. A non-basic sygus algorithm
+ // is one that is specialized for returning a single solution. Non-basic
+ // sygus algorithms currently include the PBE solver, static template
+ // inference for invariant synthesis, and single invocation techniques.
+ bool reqBasicSygus = false;
+ if (options::produceAbducts())
{
// if doing abduction, we should filter strong solutions
if (!options::sygusFilterSolMode.wasSetByUser())
{
options::sygusFilterSolMode.set(quantifiers::SYGUS_FILTER_SOL_STRONG);
}
+ // we must use basic sygus algorithms, since e.g. we require checking
+ // a sygus side condition for consistency with axioms.
+ reqBasicSygus = true;
}
if (options::sygusRewSynth() || options::sygusRewVerify()
- || options::sygusQueryGen() || options::sygusAbduct())
+ || options::sygusQueryGen())
{
// rewrite rule synthesis implies that sygus stream must be true
options::sygusStream.set(true);
@@ -1971,9 +1984,12 @@ 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,
- // static template inference for invariant synthesis, and single
- // invocation techniques.
+ // finding a single solution.
+ reqBasicSygus = true;
+ }
+ // Now, disable options for non-basic sygus algorithms, if necessary.
+ if (reqBasicSygus)
+ {
if (!options::sygusUnifPbe.wasSetByUser())
{
options::sygusUnifPbe.set(false);
@@ -2291,11 +2307,11 @@ void SmtEngine::setDefaults() {
"--sygus-expr-miner-check-timeout=N requires "
"--sygus-expr-miner-check-use-export");
}
- if (options::sygusRewSynthInput() || options::sygusAbduct())
+ if (options::sygusRewSynthInput() || options::produceAbducts())
{
std::stringstream ss;
ss << (options::sygusRewSynthInput() ? "--sygus-rr-synth-input"
- : "--sygus-abduct");
+ : "--produce-abducts");
ss << "requires --sygus-expr-miner-check-use-export";
throw OptionException(ss.str());
}
@@ -3325,10 +3341,6 @@ void SmtEnginePrivate::processAssertions() {
{
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
@@ -4961,6 +4973,96 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict)
}
}
+bool SmtEngine::getAbduct(const Expr& conj, const Type& grammarType, Expr& abd)
+{
+ SmtScope smts(this);
+
+ if (!options::produceAbducts())
+ {
+ const char* msg = "Cannot get abduct when produce-abducts options is off.";
+ throw ModalException(msg);
+ }
+ Trace("sygus-abduct") << "SmtEngine::getAbduct: conjecture " << conj
+ << std::endl;
+ std::vector<Expr> easserts = getAssertions();
+ std::vector<Node> axioms;
+ for (unsigned i = 0, size = easserts.size(); i < size; i++)
+ {
+ axioms.push_back(Node::fromExpr(easserts[i]));
+ }
+ std::vector<Node> asserts(axioms.begin(), axioms.end());
+ asserts.push_back(Node::fromExpr(conj));
+ d_sssfVarlist.clear();
+ d_sssfSyms.clear();
+ std::string name("A");
+ Node aconj = theory::quantifiers::SygusAbduct::mkAbductionConjecture(
+ name,
+ asserts,
+ axioms,
+ TypeNode::fromType(grammarType),
+ d_sssfVarlist,
+ d_sssfSyms);
+ // should be a quantified conjecture with one function-to-synthesize
+ Assert(aconj.getKind() == kind::FORALL && aconj[0].getNumChildren() == 1);
+ // remember the abduct-to-synthesize
+ d_sssf = aconj[0][0].toExpr();
+ Trace("sygus-abduct") << "SmtEngine::getAbduct: made conjecture : " << aconj
+ << ", solving for " << d_sssf << std::endl;
+ // we generate a new smt engine to do the abduction query
+ d_subsolver.reset(new SmtEngine(NodeManager::currentNM()->toExprManager()));
+ d_subsolver->setIsInternalSubsolver();
+ // get the logic
+ LogicInfo l = d_logic.getUnlockedCopy();
+ // enable everything needed for sygus
+ l.enableSygus();
+ d_subsolver->setLogic(l);
+ // assert the abduction query
+ d_subsolver->assertFormula(aconj.toExpr());
+ Trace("sygus-abduct") << " SmtEngine::getAbduct check sat..." << std::endl;
+ Result r = d_subsolver->checkSat();
+ Trace("sygus-abduct") << " SmtEngine::getAbduct result: " << r << std::endl;
+ if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
+ {
+ // get the synthesis solution
+ std::map<Expr, Expr> sols;
+ d_subsolver->getSynthSolutions(sols);
+ Assert(sols.size() == 1);
+ std::map<Expr, Expr>::iterator its = sols.find(d_sssf);
+ if (its != sols.end())
+ {
+ Node abdn = Node::fromExpr(its->second);
+ Trace("sygus-abduct")
+ << "SmtEngine::getAbduct: solution is " << abdn << std::endl;
+ if (abdn.getKind() == kind::LAMBDA)
+ {
+ abdn = abdn[1];
+ }
+ // convert back to original
+ // must replace formal arguments of abd with the free variables in the
+ // input problem that they correspond to.
+ abdn = abdn.substitute(d_sssfVarlist.begin(),
+ d_sssfVarlist.end(),
+ d_sssfSyms.begin(),
+ d_sssfSyms.end());
+
+ // convert to expression
+ abd = abdn.toExpr();
+
+ return true;
+ }
+ Trace("sygus-abduct") << "SmtEngine::getAbduct: could not find solution!"
+ << std::endl;
+ throw RecoverableModalException("Could not find solution for get-abduct.");
+ }
+ return false;
+}
+
+bool SmtEngine::getAbduct(const Expr& conj, Expr& abd)
+{
+ Type grammarType;
+ return getAbduct(conj, grammarType, abd);
+}
+
void SmtEngine::getInstantiatedQuantifiedFormulas( std::vector< Expr >& qs ) {
SmtScope smts(this);
if( d_theoryEngine ){
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 5913716e6..566777a89 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -147,6 +147,34 @@ class CVC4_PUBLIC SmtEngine {
ProofManager* d_proofManager;
/** An index of our defined functions */
DefinedFunctionMap* d_definedFunctions;
+ /** The SMT engine subsolver
+ *
+ * This is a separate copy of the SMT engine which is used for making
+ * calls that cannot be answered by this copy of the SMT engine. An example
+ * of invoking this subsolver is the get-abduct command, where we wish to
+ * solve a sygus conjecture based on the current assertions. In particular,
+ * consider the input:
+ * (assert A)
+ * (get-abduct B)
+ * In the copy of the SMT engine where these commands are issued, we maintain
+ * A in the assertion stack. To solve the abduction problem, instead of
+ * modifying the assertion stack to remove A and add the sygus conjecture
+ * (exists I. ...), we invoke a fresh copy of the SMT engine and leave the
+ * assertion stack unchaged. This copy of the SMT engine can be further
+ * queried for information regarding further solutions.
+ */
+ std::unique_ptr<SmtEngine> d_subsolver;
+ /**
+ * If applicable, the function-to-synthesize that the subsolver is solving
+ * for. This is used for the get-abduct command.
+ */
+ Expr d_sssf;
+ /**
+ * The substitution to apply to the solutions from the subsolver, used for
+ * the get-abduct command.
+ */
+ std::vector<Node> d_sssfVarlist;
+ std::vector<Node> d_sssfSyms;
/** recursive function definition abstractions for --fmf-fun */
std::map< Node, TypeNode > d_fmfRecFunctionsAbs;
std::map< Node, std::vector< Node > > d_fmfRecFunctionsConcrete;
@@ -849,6 +877,21 @@ class CVC4_PUBLIC SmtEngine {
Expr doQuantifierElimination(const Expr& e,
bool doFull,
bool strict = true) /* throw(Exception) */;
+ /**
+ * This method asks this SMT engine to find an abduct with respect to the
+ * current assertion stack (call it A) and the conjecture (call it B).
+ * If this method returns true, then abd is set to a formula C such that
+ * A ^ C is satisfiable, and A ^ B ^ C is unsatisfiable.
+ *
+ * The argument grammarType is a sygus datatype type that encodes the syntax
+ * restrictions on the shape of possible solutions.
+ *
+ * This method invokes a separate copy of the SMT engine for solving the
+ * corresponding sygus problem for generating such a solution.
+ */
+ bool getAbduct(const Expr& conj, const Type& grammarType, Expr& abd);
+ /** Same as above, but without user-provided grammar restrictions */
+ bool getAbduct(const Expr& conj, Expr& abd);
/**
* Get list of quantified formulas that were instantiated
diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
index e21d1f630..37b25163a 100644
--- a/src/theory/logic_info.cpp
+++ b/src/theory/logic_info.cpp
@@ -579,6 +579,15 @@ void LogicInfo::disableTheory(theory::TheoryId theory) {
}
}
+void LogicInfo::enableSygus()
+{
+ enableQuantifiers();
+ enableTheory(THEORY_UF);
+ enableTheory(THEORY_DATATYPES);
+ enableIntegers();
+ enableHigherOrder();
+}
+
void LogicInfo::enableIntegers() {
PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
d_logicString = "";
diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h
index a765472dd..969810a6f 100644
--- a/src/theory/logic_info.h
+++ b/src/theory/logic_info.h
@@ -201,6 +201,12 @@ public:
disableTheory(theory::THEORY_QUANTIFIERS);
}
+ /**
+ * Enable everything that is needed for sygus with respect to this logic info.
+ * This means enabling quantifiers, datatypes, UF, integers, and higher order.
+ */
+ void enableSygus();
+
// these are for arithmetic
/** Enable the use of integers in this logic. */
diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp
index 98d07fdea..6b042e294 100644
--- a/src/theory/quantifiers/expr_miner.cpp
+++ b/src/theory/quantifiers/expr_miner.cpp
@@ -91,7 +91,6 @@ void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker,
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/preprocessing/passes/sygus_abduct.cpp b/src/theory/quantifiers/sygus/sygus_abduct.cpp
index b2dc872e4..52fb60c06 100644
--- a/src/preprocessing/passes/sygus_abduct.cpp
+++ b/src/theory/quantifiers/sygus/sygus_abduct.cpp
@@ -9,18 +9,15 @@
** 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
+ ** \brief Implementation of sygus abduction utility, which
** transforms an arbitrary input into an abduction problem.
**/
-#include "preprocessing/passes/sygus_abduct.h"
+#include "theory/quantifiers/sygus/sygus_abduct.h"
#include "expr/datatype.h"
#include "expr/node_algorithm.h"
#include "printer/sygus_print_callback.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"
@@ -30,59 +27,17 @@ using namespace std;
using namespace CVC4::kind;
namespace CVC4 {
-namespace preprocessing {
-namespace passes {
+namespace theory {
+namespace quantifiers {
-SygusAbduct::SygusAbduct(PreprocessingPassContext* preprocContext)
- : PreprocessingPass(preprocContext, "sygus-abduct"){};
+SygusAbduct::SygusAbduct() {}
-PreprocessingPassResult SygusAbduct::applyInternal(
- AssertionPipeline* assertionsToPreprocess)
-{
- Trace("sygus-abduct") << "Run sygus abduct..." << std::endl;
-
- Trace("sygus-abduct-debug") << "Collect symbols..." << std::endl;
- 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;
- if (usingAssumptions)
- {
- for (size_t i = 0, astart = assertionsToPreprocess->getAssumptionsStart();
- i < astart;
- i++)
- {
- // if we are not an assumption, add it to the set of axioms
- axioms.push_back(asserts[i]);
- }
- }
-
- // the abduction grammar type we are using (null for now, until a future
- // commit)
- TypeNode abdGType;
-
- Node res = mkAbductionConjecture(asserts, axioms, abdGType);
-
- Node trueNode = NodeManager::currentNM()->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;
-}
-
-Node SygusAbduct::mkAbductionConjecture(const std::vector<Node>& asserts,
+Node SygusAbduct::mkAbductionConjecture(const std::string& name,
+ const std::vector<Node>& asserts,
const std::vector<Node>& axioms,
- TypeNode abdGType)
+ TypeNode abdGType,
+ std::vector<Node>& varlist,
+ std::vector<Node>& syms)
{
NodeManager* nm = NodeManager::currentNM();
std::unordered_set<Node, NodeHashFunction> symset;
@@ -94,9 +49,7 @@ Node SygusAbduct::mkAbductionConjecture(const std::vector<Node>& asserts,
<< "...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)
{
@@ -121,7 +74,7 @@ Node SygusAbduct::mkAbductionConjecture(const std::vector<Node>& asserts,
// make the abduction predicate to synthesize
TypeNode abdType = varlistTypes.empty() ? nm->booleanType()
: nm->mkPredicateType(varlistTypes);
- Node abd = nm->mkBoundVar("A", abdType);
+ Node abd = nm->mkBoundVar(name.c_str(), abdType);
Trace("sygus-abduct-debug") << "...finish" << std::endl;
// if provided, we will associate it with the function-to-synthesize
@@ -355,6 +308,6 @@ Node SygusAbduct::mkAbductionConjecture(const std::vector<Node>& asserts,
return res;
}
-} // namespace passes
-} // namespace preprocessing
+} // namespace quantifiers
+} // namespace theory
} // namespace CVC4
diff --git a/src/preprocessing/passes/sygus_abduct.h b/src/theory/quantifiers/sygus/sygus_abduct.h
index db40b9688..d6bbd0e3f 100644
--- a/src/preprocessing/passes/sygus_abduct.h
+++ b/src/theory/quantifiers/sygus/sygus_abduct.h
@@ -9,23 +9,25 @@
** 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.
+ ** \brief Sygus abduction utility, which transforms an arbitrary input into an
+ ** abduction problem.
**/
-#ifndef CVC4__PREPROCESSING__PASSES__SYGUS_ABDUCT_H
-#define CVC4__PREPROCESSING__PASSES__SYGUS_ABDUCT_H
+#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_ABDUCT_H
+#define CVC4__THEORY__QUANTIFIERS__SYGUS_ABDUCT_H
-#include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
+#include <string>
+#include <vector>
+#include "expr/node.h"
+#include "expr/type.h"
namespace CVC4 {
-namespace preprocessing {
-namespace passes {
+namespace theory {
+namespace quantifiers {
/** SygusAbduct
*
- * A preprocessing utility that turns a set of quantifier-free assertions into
+ * A 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:
@@ -51,34 +53,38 @@ namespace passes {
* 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
+class SygusAbduct
{
public:
- SygusAbduct(PreprocessingPassContext* preprocContext);
+ SygusAbduct();
/**
* Returns the sygus conjecture corresponding to the abduction problem for
* input problem (F above) given by asserts, and axioms (Fa above) given by
* axioms. Note that axioms is expected to be a subset of asserts.
*
+ * The argument name is the name for the abduct-to-synthesize.
+ *
* The type abdGType (if non-null) is a sygus datatype type that encodes the
* grammar that should be used for solutions of the abduction conjecture.
+ *
+ * The arguments varlist and syms specify the relationship between the free
+ * variables of asserts and the formal argument list of the
+ * abduct-to-synthesize. In particular, solutions to the synthesis conjecture
+ * will be in the form of a closed term (lambda varlist. t). The intended
+ * solution, which is a term whose free variables are a subset of asserts,
+ * is the term t { varlist -> syms }.
*/
- static Node mkAbductionConjecture(const std::vector<Node>& asserts,
+ static Node mkAbductionConjecture(const std::string& name,
+ const std::vector<Node>& asserts,
const std::vector<Node>& axioms,
- TypeNode abdGType);
-
- protected:
- /**
- * Replaces the set of assertions by an abduction sygus problem described
- * above.
- */
- PreprocessingPassResult applyInternal(
- AssertionPipeline* assertionsToPreprocess) override;
+ TypeNode abdGType,
+ std::vector<Node>& varlist,
+ std::vector<Node>& syms);
};
-} // namespace passes
-} // namespace preprocessing
+} // namespace quantifiers
+} // namespace theory
} // namespace CVC4
-#endif /* CVC4__PREPROCESSING__PASSES__SYGUS_ABDUCT_H_ */
+#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_ABDUCT_H */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback