Support get-abduct smt2 command (#3122)

3 files changed, 0 insertions, 446 deletions

diff --git a/src/preprocessing/passes/sygus_abduct.cpp b/src/preprocessing/passes/sygus_abduct.cpp
deleted file mode 100644
index b2dc872e4..000000000
--- a/src/preprocessing/passes/sygus_abduct.cpp
+++ /dev/null
@@ -1,360 +0,0 @@
-/*********************                                                        */
-/*! \file sygus_abduct.cpp
- ** \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 Implementation of sygus abduction preprocessing pass, which
- ** transforms an arbitrary input into an abduction problem.
- **/
-
-#include "preprocessing/passes/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"
-#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)
-{
-  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,
-                                        const std::vector<Node>& axioms,
-                                        TypeNode abdGType)
-{
-  NodeManager* nm = NodeManager::currentNM();
-  std::unordered_set<Node, NodeHashFunction> symset;
-  for (size_t i = 0, size = asserts.size(); i < size; i++)
-  {
-    expr::getSymbols(asserts[i], symset);
-  }
-  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);
-    }
-  }
-  // make the sygus variable list
-  Node abvl = nm->mkNode(BOUND_VAR_LIST, varlist);
-  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;
-
-  // if provided, we will associate it with the function-to-synthesize
-  if (!abdGType.isNull())
-  {
-    Assert(abdGType.isDatatype() && abdGType.getDatatype().isSygus());
-    // must convert all constructors to version with bound variables in "vars"
-    std::vector<Datatype> datatypes;
-    std::set<Type> unres;
-
-    Trace("sygus-abduct-debug") << "Process abduction type:" << std::endl;
-    Trace("sygus-abduct-debug") << abdGType.getDatatype() << std::endl;
-
-    // datatype types we need to process
-    std::vector<TypeNode> dtToProcess;
-    // datatype types we have processed
-    std::map<TypeNode, TypeNode> dtProcessed;
-    dtToProcess.push_back(abdGType);
-    std::stringstream ssutn0;
-    ssutn0 << abdGType.getDatatype().getName() << "_s";
-    TypeNode abdTNew =
-        nm->mkSort(ssutn0.str(), ExprManager::SORT_FLAG_PLACEHOLDER);
-    unres.insert(abdTNew.toType());
-    dtProcessed[abdGType] = abdTNew;
-
-    // We must convert all symbols in the sygus datatype type abdGType to
-    // apply the substitution { syms -> varlist }, where syms is the free
-    // variables of the input problem, and varlist is the formal argument list
-    // of the abduct-to-synthesize. For example, given user-provided sygus
-    // grammar:
-    //   G -> a | +( b, G )
-    // we synthesize a abduct A with two arguments x_a and x_b corresponding to
-    // a and b, and reconstruct the grammar:
-    //   G' -> x_a | +( x_b, G' )
-    // In this way, x_a and x_b are treated as bound variables and handled as
-    // arguments of the abduct-to-synthesize instead of as free variables with
-    // no relation to A. We additionally require that x_a, when printed, prints
-    // "a", which we do with a custom sygus callback below.
-
-    // We are traversing over the subfield types of the datatype to convert
-    // them into the form described above.
-    while (!dtToProcess.empty())
-    {
-      std::vector<TypeNode> dtNextToProcess;
-      for (const TypeNode& curr : dtToProcess)
-      {
-        Assert(curr.isDatatype() && curr.getDatatype().isSygus());
-        const Datatype& dtc = curr.getDatatype();
-        std::stringstream ssdtn;
-        ssdtn << dtc.getName() << "_s";
-        datatypes.push_back(Datatype(ssdtn.str()));
-        Trace("sygus-abduct-debug")
-            << "Process datatype " << datatypes.back().getName() << "..."
-            << std::endl;
-        for (unsigned j = 0, ncons = dtc.getNumConstructors(); j < ncons; j++)
-        {
-          Node op = Node::fromExpr(dtc[j].getSygusOp());
-          // apply the substitution to the argument
-          Node ops = op.substitute(
-              syms.begin(), syms.end(), varlist.begin(), varlist.end());
-          Trace("sygus-abduct-debug") << "  Process constructor " << op << " / "
-                                      << ops << "..." << std::endl;
-          std::vector<Type> cargs;
-          for (unsigned k = 0, nargs = dtc[j].getNumArgs(); k < nargs; k++)
-          {
-            TypeNode argt = TypeNode::fromType(dtc[j].getArgType(k));
-            std::map<TypeNode, TypeNode>::iterator itdp =
-                dtProcessed.find(argt);
-            TypeNode argtNew;
-            if (itdp == dtProcessed.end())
-            {
-              std::stringstream ssutn;
-              ssutn << argt.getDatatype().getName() << "_s";
-              argtNew =
-                  nm->mkSort(ssutn.str(), ExprManager::SORT_FLAG_PLACEHOLDER);
-              Trace("sygus-abduct-debug")
-                  << "    ...unresolved type " << argtNew << " for " << argt
-                  << std::endl;
-              unres.insert(argtNew.toType());
-              dtProcessed[argt] = argtNew;
-              dtNextToProcess.push_back(argt);
-            }
-            else
-            {
-              argtNew = itdp->second;
-            }
-            Trace("sygus-abduct-debug")
-                << "    Arg #" << k << ": " << argtNew << std::endl;
-            cargs.push_back(argtNew.toType());
-          }
-          // callback prints as the expression
-          std::shared_ptr<SygusPrintCallback> spc;
-          std::vector<Expr> args;
-          if (op.getKind() == LAMBDA)
-          {
-            Node opBody = op[1];
-            for (const Node& v : op[0])
-            {
-              args.push_back(v.toExpr());
-            }
-            spc = std::make_shared<printer::SygusExprPrintCallback>(
-                opBody.toExpr(), args);
-          }
-          else if (cargs.empty())
-          {
-            spc = std::make_shared<printer::SygusExprPrintCallback>(op.toExpr(),
-                                                                    args);
-          }
-          std::stringstream ss;
-          ss << ops.getKind();
-          Trace("sygus-abduct-debug")
-              << "Add constructor : " << ops << std::endl;
-          datatypes.back().addSygusConstructor(
-              ops.toExpr(), ss.str(), cargs, spc);
-        }
-        Trace("sygus-abduct-debug")
-            << "Set sygus : " << dtc.getSygusType() << " " << abvl << std::endl;
-        datatypes.back().setSygus(dtc.getSygusType(),
-                                  abvl.toExpr(),
-                                  dtc.getSygusAllowConst(),
-                                  dtc.getSygusAllowAll());
-      }
-      dtToProcess.clear();
-      dtToProcess.insert(
-          dtToProcess.end(), dtNextToProcess.begin(), dtNextToProcess.end());
-    }
-    Trace("sygus-abduct-debug")
-        << "Make " << datatypes.size() << " datatype types..." << std::endl;
-    // make the datatype types
-    std::vector<DatatypeType> datatypeTypes =
-        nm->toExprManager()->mkMutualDatatypeTypes(
-            datatypes, unres, ExprManager::DATATYPE_FLAG_PLACEHOLDER);
-    TypeNode abdGTypeS = TypeNode::fromType(datatypeTypes[0]);
-    if (Trace.isOn("sygus-abduct-debug"))
-    {
-      Trace("sygus-abduct-debug") << "Made datatype types:" << std::endl;
-      for (unsigned j = 0, ndts = datatypeTypes.size(); j < ndts; j++)
-      {
-        const Datatype& dtj = datatypeTypes[j].getDatatype();
-        Trace("sygus-abduct-debug") << "#" << j << ": " << dtj << std::endl;
-        for (unsigned k = 0, ncons = dtj.getNumConstructors(); k < ncons; k++)
-        {
-          for (unsigned l = 0, nargs = dtj[k].getNumArgs(); l < nargs; l++)
-          {
-            if (!dtj[k].getArgType(l).isDatatype())
-            {
-              Trace("sygus-abduct-debug")
-                  << "Argument " << l << " of " << dtj[k]
-                  << " is not datatype : " << dtj[k].getArgType(l) << std::endl;
-              AlwaysAssert(false);
-            }
-          }
-        }
-      }
-    }
-
-    Trace("sygus-abduct-debug")
-        << "Make sygus grammar attribute..." << std::endl;
-    Node sym = nm->mkBoundVar("sfproxy_abduct", abdGTypeS);
-    // Set the sygus grammar attribute to indicate that abdGTypeS encodes the
-    // grammar for abd.
-    theory::SygusSynthGrammarAttribute ssg;
-    abd.setAttribute(ssg, sym);
-    Trace("sygus-abduct-debug") << "Finished setting up grammar." << 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
-  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;
-
-  return res;
-}
-
-}  // namespace passes
-}  // namespace preprocessing
-}  // namespace CVC4
diff --git a/src/preprocessing/passes/sygus_abduct.h b/src/preprocessing/passes/sygus_abduct.h
deleted file mode 100644
index db40b9688..000000000
--- a/src/preprocessing/passes/sygus_abduct.h
+++ /dev/null
@@ -1,84 +0,0 @@
-/*********************                                                        */
-/*! \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);
-
-  /**
-   * 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 type abdGType (if non-null) is a sygus datatype type that encodes the
-   * grammar that should be used for solutions of the abduction conjecture.
-   */
-  static Node mkAbductionConjecture(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;
-};
-
-}  // 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 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>);