More fixes for printing sygus commands (#3812)

Towards v1 -> v2 sygus conversion.

This makes several fixes and improvements related to printing sygus commands:
(1) The logic is extended with LIA, DT, UF internally during setDefaults instead of during parsing. This is the correct place for this extension of the logic since it should be applied regardless of the parser. 5 existing logic bugs were discovered as a result of this in regressions, which are fixed by this PR.
(2) Ensures that terms in sygus grammars are printed without letification, since this is prohibited in sygus. Notice the formulas printed by constraints need to be letified (otherwise we can't convert large lustre benchmarks). Thus, the letification threshold should determine this but always be overridden for grammar terms.
(3) Ensures final options are set for all sygus-specific commands, which follows the standards prescribed by sygus v2 (all set-* commands come before other commands).

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 8faeab49184821f9a803327d079184efc8d15f1b..d915d2ab43ed1aa3b5d13b1f73af49051c0c9ada 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -755,12 +755,6 @@ Command* Smt2::setLogic(std::string name, bool fromCommand)
       warning("Logics in sygus are assumed to contain quantifiers.");
       warning("Omit QF_ from the logic to avoid this warning.");
     }
-    // get unlocked copy, modify, copy and relock
-    LogicInfo log(d_logic.getUnlockedCopy());
-    // enable everything needed for sygus
-    log.enableSygus();
-    d_logic = log;
-    d_logic.lock();
   }
 
   // Core theory belongs to every logic

diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index 28471de722222eb1c7a48845aed5479b2ef78385..886be0cfabc61fc98aa392dedda3c77ab7ce011e 100644 (file)
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -84,8 +84,9 @@ unique_ptr<Printer> Printer::makePrinter(OutputLanguage lang)
 void Printer::toStreamSygus(std::ostream& out, TNode n) const
 {
   // no sygus-specific printing associated with this printer,
-  // just print the original term
-  toStream(out, n, -1, false, 1);
+  // just print the original term, without letification (the fifth argument is
+  // set to 0).
+  toStream(out, n, -1, false, 0);
 }
 
 void Printer::toStream(std::ostream& out, const Model& m) const

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index e9a4d0a83194dd181bed33b4e3fad5bf88d36321..6fdbd4adb8305e315712f80660aaa3390116fea1 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1522,7 +1522,8 @@ void Smt2Printer::toStreamSygus(std::ostream& out, TNode n) const
         {
           out << "(";
         }
-        out << dt[cIndex].getSygusOp();
+        // print operator without letification (the fifth argument is set to 0).
+        toStream(out, dt[cIndex].getSygusOp(), -1, false, 0);
         if (n.getNumChildren() > 0)
         {
           for (Node nc : n)
@@ -1537,15 +1538,12 @@ void Smt2Printer::toStreamSygus(std::ostream& out, TNode n) const
     }
   }
   Node p = n.getAttribute(theory::SygusPrintProxyAttribute());
-  if (!p.isNull())
+  if (p.isNull())
   {
-    out << p;
-  }
-  else
-  {
-    // cannot convert term to analog, print original
-    out << n;
+    p = n;
   }
+  // cannot convert term to analog, print original, without letification.
+  toStream(out, p, -1, false, 0);
 }
 
 static void toStream(std::ostream& out, const AssertCommand* c)

diff --git a/src/printer/sygus_print_callback.cpp b/src/printer/sygus_print_callback.cpp
index ae1d97c64c21f3313be6d69d59d00521b7af59d9..92a89a18ee970cf919b4327595f23322b32f8f0d 100644 (file)
--- a/src/printer/sygus_print_callback.cpp
+++ b/src/printer/sygus_print_callback.cpp
@@ -78,8 +78,9 @@ void SygusExprPrintCallback::toStreamSygus(const Printer* p,
     sbody =
         sbody.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
 
+    // print to stream without letification
     std::stringstream body_out;
-    body_out << sbody;
+    p->toStream(body_out, sbody, -1, false, 0);
 
     // do string substitution
     Assert(e.getNumChildren() == d_args.size());

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 081e36953abb93bf1af3c49c4691ed4731874ee2..915dc603efccebd9c96ae2009cce8afb682b7eb8 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1313,13 +1313,18 @@ void SmtEngine::setDefaults() {
     {
       // 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();
     }
   }
 
+  // We now know whether the input is sygus. Update the logic to incorporate
+  // the theories we need internally for handling sygus problems.
+  if (is_sygus)
+  {
+    d_logic = d_logic.getUnlockedCopy();
+    d_logic.enableSygus();
+    d_logic.lock();
+  }
+
   // sygus core connective requires unsat cores
   if (options::sygusCoreConnective())
   {
@@ -3983,6 +3988,8 @@ Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore)
 
 void SmtEngine::declareSygusVar(const std::string& id, Expr var, Type type)
 {
+  SmtScope smts(this);
+  finalOptionsAreSet();
   d_private->d_sygusVars.push_back(Node::fromExpr(var));
   Trace("smt") << "SmtEngine::declareSygusVar: " << var << "\n";
   Dump("raw-benchmark") << DeclareSygusVarCommand(id, var, type);
@@ -3991,6 +3998,8 @@ void SmtEngine::declareSygusVar(const std::string& id, Expr var, Type type)
 
 void SmtEngine::declareSygusPrimedVar(const std::string& id, Type type)
 {
+  SmtScope smts(this);
+  finalOptionsAreSet();
   // do nothing (the command is spurious)
   Trace("smt") << "SmtEngine::declareSygusPrimedVar: " << id << "\n";
   // don't need to set that the conjecture is stale
@@ -4000,6 +4009,8 @@ void SmtEngine::declareSygusFunctionVar(const std::string& id,
                                         Expr var,
                                         Type type)
 {
+  SmtScope smts(this);
+  finalOptionsAreSet();
   d_private->d_sygusVars.push_back(Node::fromExpr(var));
   Trace("smt") << "SmtEngine::declareSygusFunctionVar: " << var << "\n";
   Dump("raw-benchmark") << DeclareSygusVarCommand(id, var, type);
@@ -4044,6 +4055,7 @@ void SmtEngine::declareSynthFun(const std::string& id,
 void SmtEngine::assertSygusConstraint(Expr constraint)
 {
   SmtScope smts(this);
+  finalOptionsAreSet();
   d_private->d_sygusConstraints.push_back(constraint);
 
   Trace("smt") << "SmtEngine::assertSygusConstrant: " << constraint << "\n";
@@ -4058,6 +4070,7 @@ void SmtEngine::assertSygusInvConstraint(const Expr& inv,
                                          const Expr& post)
 {
   SmtScope smts(this);
+  finalOptionsAreSet();
   // build invariant constraint
 
   // get variables (regular and their respective primed versions)

diff --git a/test/regress/regress0/sygus/sygus-uf.sy b/test/regress/regress0/sygus/sygus-uf.sy
index 1b060637ae789469b54be8de8d38df524a5fd74c..d506dd5b21ffd8e126f918c13ee3416451a1cdea 100644 (file)
--- a/test/regress/regress0/sygus/sygus-uf.sy
+++ b/test/regress/regress0/sygus/sygus-uf.sy
@@ -1,6 +1,6 @@
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --sygus-out=status --uf-ho
 ; EXPECT: unsat
-(set-logic LIA)
+(set-logic UFLIA)
 
 (declare-fun uf (Int) Int)
 

diff --git a/test/regress/regress1/sygus/constant-bool-si-all.sy b/test/regress/regress1/sygus/constant-bool-si-all.sy
index eee7956f429519bd10cabf38360217a2701c445c..45d49e75b43f74d53e172c750c0dcd2edb4ade0b 100644 (file)
--- a/test/regress/regress1/sygus/constant-bool-si-all.sy
+++ b/test/regress/regress1/sygus/constant-bool-si-all.sy
@@ -1,6 +1,6 @@
 ; EXPECT: unsat
 ; COMMAND-LINE: --sygus-out=status
-(set-logic SAT)
+(set-logic LIA)
 (synth-fun f () Bool)
 (synth-fun g () Bool)
 (synth-fun h () Bool)

diff --git a/test/regress/regress1/sygus/constant-dec-tree-bug.sy b/test/regress/regress1/sygus/constant-dec-tree-bug.sy
index 7229dea2ee43aba14e1ad9e510b05f332145c2f8..e20520a4a200b447e47fe77e05422d5ce1453e57 100644 (file)
--- a/test/regress/regress1/sygus/constant-dec-tree-bug.sy
+++ b/test/regress/regress1/sygus/constant-dec-tree-bug.sy
@@ -1,7 +1,7 @@
 ; EXPECT: unsat
 ; COMMAND-LINE: --sygus-out=status --sygus-unif-pi=complete
 
-(set-logic SAT)
+(set-logic LIA)
 (synth-fun u ((x Int)) Int)
 (synth-fun f () Bool)
 (synth-fun g () Bool)

diff --git a/test/regress/regress1/sygus/sygus-uf-ex.sy b/test/regress/regress1/sygus/sygus-uf-ex.sy
index b9731de0f6f442256a89844317bd742009126a71..66880eafa17d8315eeef29723621f3552a9dcf5e 100644 (file)
--- a/test/regress/regress1/sygus/sygus-uf-ex.sy
+++ b/test/regress/regress1/sygus/sygus-uf-ex.sy
@@ -1,6 +1,6 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
-(set-logic LIA)
+; COMMAND-LINE: --sygus-out=status --uf-ho
+(set-logic UFLIA)
 (declare-fun uf ( Int ) Int)
 (synth-fun f ((x Int) (y Int)) Bool
 ((Start Bool (true false

diff --git a/test/regress/regress1/sygus/tester.sy b/test/regress/regress1/sygus/tester.sy
index bf1cd15766b14ace1359222992c89f7020728b50..282bc122c01be963ca997f9f49c56fe81d4cb37c 100644 (file)
--- a/test/regress/regress1/sygus/tester.sy
+++ b/test/regress/regress1/sygus/tester.sy
@@ -1,7 +1,7 @@
 ; EXPECT: unsat
 ; COMMAND-LINE: --sygus-out=status
 
-(set-logic SLIA)
+(set-logic DTSLIA)
 (declare-datatype DT ((A (a Int)) (B (b String)) (JSBool (jsBool Bool))))
 
 (define-fun isA ((i DT)) Bool ((_ is A) i) )