Also extends to non-trivial unit test of SynthResult.
Note this also changes the expected output when using --sygus-out=status from unsat/sat/unknown to feasible/infeasible/fail (the option is used mostly just for our regressions). The output mode status-or-def is now equivalent to standard and is hence deleted.
{slv.mkTerm(ADD, {max_x_y, min_x_y}), slv.mkTerm(ADD, {varX, varY})}));
// print solutions if available
- if (slv.checkSynth().isUnsat())
+ if (slv.checkSynth().hasSolution())
{
// Output should be equivalent to:
// (
slv.mkTerm(EQUAL, {{id1_x, id2_x, id3_x, id4_x, varX}}));
// print solutions if available
- if (slv.checkSynth().isUnsat())
+ if (slv.checkSynth().hasSolution())
{
// Output should be equivalent to:
// (
slv.addSygusInvConstraint(inv_f, pre_f, trans_f, post_f);
// print solutions if available
- if (slv.checkSynth().isUnsat())
+ if (slv.checkSynth().hasSolution())
{
// Output should be equivalent to:
// (
slv.mkTerm(EQUAL, slv.mkTerm(ADD, max_x_y, min_x_y), slv.mkTerm(ADD, varX, varY)));
// print solutions if available
- if (slv.checkSynth().isUnsat())
+ if (slv.checkSynth().hasSolution())
{
// Output should be equivalent to:
// (
slv.addSygusConstraint(slv.mkTerm(EQUAL, new Term[] {id1_x, id2_x, id3_x, id4_x, varX}));
// print solutions if available
- if (slv.checkSynth().isUnsat())
+ if (slv.checkSynth().hasSolution())
{
// Output should be equivalent to:
// (
slv.addSygusInvConstraint(inv_f, pre_f, trans_f, post_f);
// print solutions if available
- if (slv.checkSynth().isUnsat())
+ if (slv.checkSynth().hasSolution())
{
// Output should be equivalent to:
// (
Kind.Equal, slv.mkTerm(Kind.Add, max_x_y, min_x_y), slv.mkTerm(Kind.Add, varX, varY)))
# print solutions if available
- if (slv.checkSynth().isUnsat()):
+ if (slv.checkSynth().hasSolution()):
# Output should be equivalent to:
# (define-fun max ((x Int) (y Int)) Int (ite (<= x y) y x))
# (define-fun min ((x Int) (y Int)) Int (ite (<= x y) x y))
slv.addSygusConstraint(slv.mkTerm(Kind.And, [slv.mkTerm(Kind.Equal, id1_x, id2_x), slv.mkTerm(Kind.Equal, id1_x, id3_x), slv.mkTerm(Kind.Equal, id1_x, id4_x), slv.mkTerm(Kind.Equal, id1_x, varX)]))
# print solutions if available
- if (slv.checkSynth().isUnsat()):
+ if (slv.checkSynth().hasSolution()):
# Output should be equivalent to:
# (define-fun id1 ((x Int)) Int (+ x (+ x (- x))))
# (define-fun id2 ((x Int)) Int x)
slv.addSygusInvConstraint(inv_f, pre_f, trans_f, post_f)
# print solutions if available
- if slv.checkSynth().isUnsat():
+ if slv.checkSynth().hasSolution():
# Output should be equivalent to:
# (define-fun inv-f ((x Int)) Bool (not (>= x 11)))
terms = [inv_f]
CVC5_API_TRY_CATCH_END;
}
-Result Solver::checkSynth() const
+SynthResult Solver::checkSynth() const
{
CVC5_API_TRY_CATCH_BEGIN;
CVC5_API_CHECK(d_slv->getOptions().quantifiers.sygus)
CVC5_API_TRY_CATCH_END;
}
-Result Solver::checkSynthNext() const
+SynthResult Solver::checkSynthNext() const
{
CVC5_API_TRY_CATCH_BEGIN;
CVC5_API_CHECK(d_slv->getOptions().quantifiers.sygus)
* (check-synth)
* \endverbatim
*
- * @return the result of the check, which is unsat if the check succeeded,
- * in which case solutions are available via getSynthSolutions.
+ * @return the result of the check, which is "solution" if the check found a
+ * solution in which case solutions are available via
+ * getSynthSolutions, "no solution" if it was determined there is no
+ * solution, or "unknown" otherwise.
*/
- Result checkSynth() const;
+ SynthResult checkSynth() const;
/**
* Try to find a next solution for the synthesis conjecture corresponding to
* (check-synth-next)
* \endverbatim
*
- * @return the result of the check, which is unsat if the check succeeded,
- * in which case solutions are available via getSynthSolutions.
+ * @return the result of the check, which is "solution" if the check found a
+ * solution in which case solutions are available via
+ * getSynthSolutions, "no solution" if it was determined there is no
+ * solution, or "unknown" otherwise.
*/
- Result checkSynthNext() const;
+ SynthResult checkSynthNext() const;
/**
* Get the synthesis solution of the given term. This method should be called
* {@code
* ( check-synth )
* }
- * @return the result of the check, which is unsat if the check succeeded,
- * in which case solutions are available via getSynthSolutions.
+ * @return the result of the check, which is "solution" if the check found a
+ * solution in which case solutions are available via
+ * getSynthSolutions, "no solution" if it was determined there is no
+ * solution, or "unknown" otherwise.
*/
- public Result checkSynth()
- {
+ public SynthResult checkSynth() {
long resultPointer = checkSynth(pointer);
- return new Result(this, resultPointer);
+ return new SynthResult(this, resultPointer);
}
private native long checkSynth(long pointer);
* {@code
* ( check-synth-next )
* }
- * @return the result of the check, which is UNSAT if the check succeeded,
- * in which case solutions are available via getSynthSolutions.
+ * @return the result of the check, which is "solution" if the check found a
+ * solution in which case solutions are available via
+ * getSynthSolutions, "no solution" if it was determined there is no
+ * solution, or "unknown" otherwise.
*/
- public Result checkSynthNext()
- {
+ public SynthResult checkSynthNext() {
long resultPointer = checkSynthNext(pointer);
- return new Result(this, resultPointer);
+ return new SynthResult(this, resultPointer);
}
private native long checkSynthNext(long pointer);
{
CVC5_JAVA_API_TRY_CATCH_BEGIN;
Solver* solver = reinterpret_cast<Solver*>(pointer);
- Result* retPointer = new Result(solver->checkSynth());
+ SynthResult* retPointer = new SynthResult(solver->checkSynth());
return reinterpret_cast<jlong>(retPointer);
CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
}
{
CVC5_JAVA_API_TRY_CATCH_BEGIN;
Solver* solver = reinterpret_cast<Solver*>(pointer);
- Result* retPointer = new Result(solver->checkSynthNext());
+ SynthResult* retPointer = new SynthResult(solver->checkSynthNext());
return reinterpret_cast<jlong>(retPointer);
CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
}
void addSygusInvConstraint(Term inv_f, Term pre_f, Term trans_f, Term post_f) except +
Term synthFun(const string& symbol, const vector[Term]& bound_vars, Sort sort) except +
Term synthFun(const string& symbol, const vector[Term]& bound_vars, Sort sort, Grammar grammar) except +
- Result checkSynth() except +
- Result checkSynthNext() except +
+ SynthResult checkSynth() except +
+ SynthResult checkSynthNext() except +
Term getSynthSolution(Term t) except +
vector[Term] getSynthSolutions(const vector[Term]& terms) except +
Term synthInv(const string& symbol, const vector[Term]& bound_vars) except +
( check-synth )
- :return: the result of the synthesis conjecture.
+ :return: the result of the check, which is "solution" if the check
+ found a solution in which case solutions are available via
+ getSynthSolutions, "no solution" if it was determined there is
+ no solution, or "unknown" otherwise.
"""
- cdef Result r = Result()
+ cdef SynthResult r = SynthResult()
r.cr = self.csolver.checkSynth()
return r
( check-synth )
- :return: the result of the check, which is unsat if the check succeeded,
- in which case solutions are available via getSynthSolutions.
+ :return: the result of the check, which is "solution" if the check
+ found a solution in which case solutions are available via
+ getSynthSolutions, "no solution" if it was determined there is
+ no solution, or "unknown" otherwise.
"""
- cdef Result r = Result()
+ cdef SynthResult r = SynthResult()
r.cr = self.csolver.checkSynthNext()
return r
[[option.mode.STATUS_AND_DEF]]
name = "status-and-def"
help = "Print status followed by definition corresponding to solution."
-[[option.mode.STATUS_OR_DEF]]
- name = "status-or-def"
- help = "Print status if infeasible, or definition corresponding to solution if feasible."
[[option.mode.STANDARD]]
name = "sygus-standard"
help = "Print based on SyGuS standard."
d_commandStatus = CommandSuccess::instance();
d_solution.clear();
// check whether we should print the status
- if (!d_result.isUnsat()
+ if (!d_result.hasSolution()
|| options::sygusOut() == options::SygusSolutionOutMode::STATUS_AND_DEF
|| options::sygusOut() == options::SygusSolutionOutMode::STATUS)
{
- if (options::sygusOut() == options::SygusSolutionOutMode::STANDARD)
+ if (d_result.hasSolution())
{
- d_solution << "fail" << endl;
+ d_solution << "feasible" << std::endl;
+ }
+ else if (d_result.hasNoSolution())
+ {
+ d_solution << "infeasible" << std::endl;
}
else
{
- d_solution << d_result << endl;
+ d_solution << "fail" << std::endl;
}
}
// check whether we should print the solution
- if (d_result.isUnsat()
+ if (d_result.hasSolution()
&& options::sygusOut() != options::SygusSolutionOutMode::STATUS)
{
std::vector<api::Term> synthFuns = sm->getFunctionsToSynthesize();
}
}
-api::Result CheckSynthCommand::getResult() const { return d_result; }
+api::SynthResult CheckSynthCommand::getResult() const { return d_result; }
void CheckSynthCommand::printResult(std::ostream& out) const
{
if (!ok())
public:
CheckSynthCommand(bool isNext = false) : d_isNext(isNext){};
/** returns the result of the check-synth call */
- api::Result getResult() const;
+ api::SynthResult getResult() const;
/** prints the result of the check-synth-call */
void printResult(std::ostream& out) const override;
/** invokes this command
/** Whether this is a check-synth-next call */
bool d_isNext;
/** result of the check-synth call */
- api::Result d_result;
+ api::SynthResult d_result;
/** string stream that stores the output of the solution */
std::stringstream d_solution;
};
d_sygusSolver->assertSygusInvConstraint(inv, pre, trans, post);
}
-Result SolverEngine::checkSynth(bool isNext)
+SynthResult SolverEngine::checkSynth(bool isNext)
{
SolverEngineScope smts(this);
finishInit();
"Cannot check-synth-next unless immediately preceded by a successful "
"call to check-synth(-next).");
}
- Result r = d_sygusSolver->checkSynth(*d_asserts, isNext);
+ SynthResult r = d_sygusSolver->checkSynth(*d_asserts, isNext);
d_state->notifyCheckSynthResult(r);
return r;
}
#include "smt/smt_mode.h"
#include "theory/logic_info.h"
#include "util/result.h"
+#include "util/synth_result.h"
namespace cvc5 {
*
* @throw Exception
*/
- Result checkSynth(bool isNext = false);
+ SynthResult checkSynth(bool isNext = false);
/*------------------------- end of sygus commands ------------------------*/
}
}
-void SolverEngineState::notifyCheckSatResult(bool hasAssumptions, Result r)
+void SolverEngineState::notifyCheckSatResult(bool hasAssumptions,
+ const Result& r)
{
d_needPostsolve = true;
}
}
-void SolverEngineState::notifyCheckSynthResult(Result r)
+void SolverEngineState::notifyCheckSynthResult(const SynthResult& r)
{
- if (r.getStatus() == Result::UNSAT)
+ if (r.getStatus() == SynthResult::SOLUTION)
{
// successfully generated a synthesis solution, update to abduct state
d_smtMode = SmtMode::SYNTH;
#include "smt/env_obj.h"
#include "smt/smt_mode.h"
#include "util/result.h"
+#include "util/synth_result.h"
namespace cvc5 {
* If so, we pop a context.
* @param r The result of the check-sat call.
*/
- void notifyCheckSatResult(bool hasAssumptions, Result r);
+ void notifyCheckSatResult(bool hasAssumptions, const Result& r);
/**
* Notify that the result of the last check-synth or check-synth-next was r.
* @param r The result of the check-synth or check-synth-next call.
*/
- void notifyCheckSynthResult(Result r);
+ void notifyCheckSynthResult(const SynthResult& r);
/**
* Notify that we finished an abduction query, where success is whether the
* command was successful. This is managed independently of the above
d_sygusConjectureStale = true;
}
-Result SygusSolver::checkSynth(Assertions& as, bool isNext)
+SynthResult SygusSolver::checkSynth(Assertions& as, bool isNext)
{
Trace("smt") << "SygusSolver::checkSynth" << std::endl;
// if applicable, check if the subsolver is the correct one
// The result returned by the above call is typically "unknown", which may
// or may not correspond to a state in which we solved the conjecture
// successfully. Instead we call getSynthSolutions below. If this returns
- // true, then we were successful. In this case, we set the result to "unsat",
- // since the synthesis conjecture was negated when asserted to the subsolver.
+ // true, then we were successful. In this case, we set the synthesis result to
+ // "solution".
//
// This behavior is done for 2 reasons:
// (1) if we do not negate the synthesis conjecture, the subsolver in some
//
// Thus, we use getSynthSolutions as means of knowing the conjecture was
// solved.
+ SynthResult sr;
std::map<Node, Node> sol_map;
if (getSynthSolutions(sol_map))
{
- // if we have solutions, we return "unsat" by convention
- r = Result(Result::UNSAT);
+ // if we have solutions, we return "solution"
+ sr = SynthResult(SynthResult::SOLUTION);
// Check that synthesis solutions satisfy the conjecture
if (options().smt.checkSynthSol)
{
else
{
// otherwise, we return "unknown"
- r = Result(Result::UNKNOWN, Result::UNKNOWN_REASON);
+ sr = SynthResult(SynthResult::UNKNOWN, Result::UNKNOWN_REASON);
}
- return r;
+ return sr;
}
bool SygusSolver::getSynthSolutions(std::map<Node, Node>& solMap)
#include "expr/type_node.h"
#include "smt/assertions.h"
#include "smt/env_obj.h"
-#include "util/result.h"
+#include "util/synth_result.h"
namespace cvc5 {
* in which f1...fn are the functions-to-synthesize, v1...vm are the declared
* universal variables and F is the set of declared constraints.
*/
- Result checkSynth(Assertions& as, bool isNext);
+ SynthResult checkSynth(Assertions& as, bool isNext);
/**
* Get synth solution.
*
Trace("sygus-interpol")
<< " SygusInterpol::solveInterpolation check synth..." << std::endl;
- Result r = d_subSolver->checkSynth();
+ SynthResult r = d_subSolver->checkSynth();
Trace("sygus-interpol") << " SygusInterpol::solveInterpolation result: " << r
<< std::endl;
- if (r.getStatus() == Result::UNSAT)
+ if (r.getStatus() == SynthResult::SOLUTION)
{
return findInterpol(d_subSolver.get(), interpol, d_itp);
}
Trace("sygus-interpol")
<< " SygusInterpol::solveInterpolationNext check synth..." << std::endl;
// invoke the check-synth with isNext = true.
- Result r = d_subSolver->checkSynth(true);
+ SynthResult r = d_subSolver->checkSynth(true);
Trace("sygus-interpol") << " SygusInterpol::solveInterpolationNext result: "
<< r << std::endl;
- if (r.getStatus() == Result::UNSAT)
+ if (r.getStatus() == SynthResult::SOLUTION)
{
return findInterpol(d_subSolver.get(), interpol, d_itp);
}
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status
(set-logic LIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-si-abort --decision=internal --cegqi --sygus-out=status
(set-logic BV)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic ALIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --sygus-out=status
(set-logic LIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status
(set-logic LIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic SAT)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic ALL)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic ALL)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status --decision=justification
(set-logic LIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status
(set-logic LIA)
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
-; EXPECT: unsat
+; EXPECT: feasible
(set-logic LIA)
(declare-datatypes ((List 0)) (((cons (head Int) (tail List)) (nil))))
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
-; EXPECT: unsat
+; EXPECT: feasible
(set-logic ALL)
(declare-datatypes ((IntRange 0))
; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-si=none
-; EXPECT: unsat
+; EXPECT: feasible
(set-logic BV)
; COMMAND-LINE: --sygus-out=status
-; EXPECT: unsat
+; EXPECT: feasible
(set-logic HO_ALL)
(synth-fun f ((x Int)) Int)
(synth-fun g ((x Int)) Int)
; COMMAND-LINE: -i --sygus-out=status
-;EXPECT: unsat
-;EXPECT: unsat
+;EXPECT: feasible
+;EXPECT: feasible
(set-logic LIA)
(synth-fun f ((x Int) (y Int)) Int
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
-;EXPECT: unsat
+;EXPECT: feasible
(set-logic LIA)
(synth-inv inv-f ((x Int) (y Int) (b Bool)))
(define-fun pre-f ((x Int) (y Int) (b Bool)) Bool
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic ALL)
(declare-var A Bool)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic ALL)
(synth-fun args_0_refinement_0
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --sygus-out=status
(set-logic NIA)
(synth-fun patternGen ((i Int)) Int
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic ALL)
(declare-datatypes (( List 1)) ( (par (T) ((nil) (cons (head T) (tail (List T)))))))
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status
; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-unif-pi=complete --sygus-out=status
(set-logic LIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status
(set-logic LIA)
(define-fun letf ((z Int)) Int (+ z z))
; EXPECT-ERROR: no-logic.sy:8.10: cvc5 will make all theories available.
; EXPECT-ERROR: no-logic.sy:8.10: Consider setting a stricter logic for (likely) better performance.
; EXPECT-ERROR: no-logic.sy:8.10: To suppress this warning in the future use (set-logic ALL).
-; EXPECT: unsat
+; EXPECT: feasible
(synth-fun f ((x Int)) Int
((Start Int))
(
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic LIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic LIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status
(set-logic BV)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic BV)
; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status -q
-; EXPECT: unknown
+; EXPECT: fail
(set-logic LIA)
(synth-fun P ((x Int)) Bool)
(constraint (P 54))
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic LRA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic SLIA)
(synth-fun f ((firstname String) (lastname String)) String
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
-; EXPECT: unsat
+; EXPECT: feasible
(set-logic ALL)
(synth-fun f ((x0 Bool)) Bool
((B Bool) (I Int))
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
-; EXPECT: unsat
+; EXPECT: feasible
(set-logic HO_ALL)
(declare-var uf (-> Int Int))
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic LIA)
(synth-fun f ((x Int)) Int ((Start Int)) ((Start Int ((- 1)))))
-; EXPECT: unknown
+; EXPECT: fail
; COMMAND-LINE: --lang=sygus2 --sygus-out=status -q
(set-logic SLIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-qe-preproc --cegqi-full --sygus-out=status --sygus-si=all
(set-logic BV)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
; COMMAND-LINE: --lang=sygus2 --sygus-out=status --cegis-sample=use
(set-logic LIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic ABV)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic ABV)
; COMMAND-LINE: --sygus-out=status
-; EXPECT: unsat
+; EXPECT: feasible
(set-logic ALL)
(declare-sort U 0)
(synth-fun f ((x (Array U Int)) (y U)) Bool)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status
(set-logic LIA)
(synth-fun findIdx ((y1 Int) (y2 Int) (k1 Int)) Int ((Start Int) (BoolExpr Bool)) ((Start Int ( 0 1 2 y1 y2 k1 (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start)))))
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status --decision=justification
(set-logic LIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status
(set-logic LIA)
(synth-fun findSum ( (y1 Int) (y2 Int) )Int ((Start Int) (BoolExpr Bool)) ((Start Int ( 0 1 2 y1 y2 (+ Start Start) (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start)))))
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic BV)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-unif-pi=cond-enum-igain --decision=justification
(set-logic LIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-inv-templ=post --sygus-out=status
(set-logic LIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-unif-pi=complete --sygus-bool-ite-return-const --sygus-out=status
(set-logic LIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-inv-templ=pre --sygus-out=status
(set-logic LIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status --decision=justification
(set-logic ALL)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --sygus-out=status --sygus-repair-const --lang=sygus2 --sygus-grammar-cons=any-const
(set-logic LIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic LIA)
; COMMAND-LINE: --sygus-si=all --sygus-out=status
-; EXPECT: unsat
+; EXPECT: feasible
(set-logic LIA)
; COMMAND-LINE: --sygus-si=all --sygus-out=status
-; EXPECT: unsat
+; EXPECT: feasible
(set-logic LIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --sygus-out=status --lang=sygus2
(set-logic BV)
(synth-fun f (( x (_ BitVec 32))) (_ BitVec 32)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic LIA)
(synth-fun f () Bool)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-unif-pi=complete
(set-logic LIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status --no-sygus-pbe --sygus-repair-const
(set-logic BV)
(synth-fun f ( (x (_ BitVec 64))) (_ BitVec 64)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic LIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic BV)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-si-abort --decision=internal --sygus-si-rcons=try --sygus-out=status
(set-logic BV)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic BV)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic NIA)
; COMMAND-LINE: --sygus-out=status
-; EXPECT: unsat
+; EXPECT: feasible
(set-logic LIA)
;declare enums
-; EXPECT: unsat\r
+; EXPECT: feasible\r
; COMMAND-LINE: --lang=sygus2 --sygus-out=status\r
\r
(set-logic SLIA)\r
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status
(set-logic DTLIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status
(set-logic LIA)
(synth-fun f ((x Int)) Int
; COMMAND-LINE: --sygus-si=all --sygus-out=status
-; EXPECT: unsat
+; EXPECT: feasible
; This regression tests the behavior of the reconstruction algorithm when the
; term to reconstruct contains two equivalent sub-terms, but one is easier to
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-si=none --sygus-enum=fast
(set-logic ALL)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic HO_ALL)
(declare-sort S 0)
-; EXPECT: unsat\r
+; EXPECT: feasible\r
; COMMAND-LINE: --lang=sygus2 --sygus-out=status\r
\r
(set-logic ALL)\r
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --sygus-out=status --lang=sygus2 --sygus-enum=fast
(set-logic ALL)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic LIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic BV)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
; COMMAND-LINE: --lang=sygus2 --sygus-out=status --cegis-sample=trust --no-check-synth-sol
(set-logic BV)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic BV)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic BV)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status
(set-logic BV)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status
(set-logic BV)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic HO_ALL)
(synth-fun f ((y (-> Int Int)) (z Int)) Int)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic BV)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic BV)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic BV)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic BV)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic BV)
; COMMAND-LINE: -i --sygus-out=status
-;EXPECT: unsat
-;EXPECT: unsat
-;EXPECT: unsat
-;EXPECT: unsat
+;EXPECT: feasible
+;EXPECT: feasible
+;EXPECT: feasible
+;EXPECT: feasible
(set-logic LIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status --no-sygus-pbe --sygus-si=none --sygus-grammar-cons=any-term-concise
(set-logic LIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic LIA)
(synth-inv inv-f ((x Int) (y Int) (b Bool)))
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic LIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic LIA)
(synth-inv inv-f ((x Int) (y Int) (b Bool)))
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic LIA)
(synth-fun inv ((l Int)) Bool
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic SLIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic SLIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --sygus-out=status
(set-logic ALL)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic LIA)
(declare-var x Int)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic ALL)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --sygus-out=status --sygus-enum=smart --lang=sygus2
(set-logic ALL)
(synth-fun f
-; EXPECT: unknown
+; EXPECT: fail
; COMMAND-LINE: --lang=sygus2 --sygus-out=status -q
(set-logic ALL)
(synth-fun inv-fn ((i Int) (x (Array Int Int)) (c Int)) Bool)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --sygus-out=status --lang=sygus2
(set-logic ALL)
(synth-fun f
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status --sygus-add-const-grammar
(set-logic LIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic LIA)
(define-fun letf ((z Int) (v1 Int) (v2 Int)) Bool
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status
(set-logic ALL)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --sygus-out=status --lang=sygus2
(set-logic HO_ALL)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-repair-const
(set-logic BV)
; COMMAND-LINE: --sygus-si=all --sygus-si-rcons-limit=0 --sygus-out=status
-; EXPECT: unsat
+; EXPECT: feasible
(set-logic LIA)
; COMMAND-LINE: --sygus-si=all --sygus-si-rcons=all-limit --sygus-si-rcons-limit=0 --sygus-out=status
; ERROR-SCRUBBER: grep -o "reconstruction to syntax failed."
; EXPECT-ERROR: reconstruction to syntax failed.
-; EXPECT: unknown
+; EXPECT: fail
; REQUIRES: no-competition
(set-logic LIA)
; COMMAND-LINE: --sygus-si=all --sygus-si-rcons=try --sygus-out=status
-; EXPECT: unsat
+; EXPECT: feasible
(set-logic LIA)
; COMMAND-LINE: --sygus-si=all --sygus-si-rcons=try --sygus-out=status
; ERROR-SCRUBBER: grep -o "reconstruction to syntax failed."
; EXPECT-ERROR: reconstruction to syntax failed.
-; EXPECT: unknown
+; EXPECT: fail
; REQUIRES: no-competition
(set-logic LIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status
(set-logic LIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status --cegqi-bv
(set-logic BV)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic LIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic LIA)
(synth-fun f ((x Int)) Int
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic LIA)
(synth-fun f ((x Int)) Int
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status --nl-ext-tplanes
(set-logic NIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic LIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic LIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --sygus-out=status --lang=sygus2 --no-check-synth-sol
(set-logic ALL)
; reliability
(define-fun rel () Real 0.7)
-; new chance of success
+; new chance of feasible
(define-fun updateReal ((addP Real) (currP Real)) Real
(+ currP (* (- 1.0 currP) addP))
)
(let ((dst_pair (mkPair dst pck)))
(let ((src_pair (mkPair actor pck)))
(let ((chSuccess (ite (select prevRcv src_pair) rel 0.0)))
- ; success and failure
+ ; feasible and failure
(appendStateToPState
(mkState (store prevRcv dst_pair true))
(* r chSuccess)
(let ((dst_pair (mkPair actor pck)))
(let ((src_pair (mkPair src pck)))
(let ((chSuccess (ite (select prevRcv src_pair) rel 0.0)))
- ; success and failure
+ ; feasible and failure
(appendStateToPState
(mkState (store prevRcv dst_pair true))
(* r chSuccess)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic BV)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --sygus-out=status --lang=sygus2
(set-logic LIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --sygus-out=status --lang=sygus2
(set-logic BV)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-si-abort --decision=internal --sygus-si-rcons=try --sygus-out=status
(set-logic BV)
-; EXPECT: unsat\r
+; EXPECT: feasible\r
; COMMAND-LINE: --lang=sygus2 --sygus-out=status\r
(set-logic BV)\r
\r
; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status --sygus-fair=direct\r
-; EXPECT: unsat\r
+; EXPECT: feasible\r
(set-logic SLIA)\r
\r
(synth-fun f ((name String)) String\r
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-unif-pi=complete --sygus-out=status
(set-logic LIA)
; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status --sygus-arg-relevant
-; EXPECT: unsat
+; EXPECT: feasible
(set-logic LIA)
(synth-fun f ((x1 Int) (x2 Int) (x3 Int) (x4 Int) (x5 Int) (x6 Int) (x7 Int) (x8 Int) (x9 Int) (x10 Int)) Int)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status --sygus-qe-preproc
(set-logic LIA)
; COMMAND-LINE: --sygus-enum=random --sygus-out=status
-; EXPECT: unsat
+; EXPECT: feasible
(set-logic BV)
; COMMAND-LINE: --sygus-enum=random --sygus-out=status
-; EXPECT: unsat
+; EXPECT: feasible
(set-logic BV)
(set-option :sygus-enum-random-p 0)
; COMMAND-LINE: --sygus-enum=random --sygus-out=status
-; EXPECT: unsat
+; EXPECT: feasible
(set-logic BV)
(set-option :sygus-enum-random-p 1)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic SLIA)
(synth-fun f () RegLan ((Start RegLan) (Tokens String)) (
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status --no-sygus-pbe --sygus-si=none --sygus-grammar-cons=any-term-concise
(set-logic LRA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-si=none
(set-logic LRA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --sygus-out=status --lang=sygus2
(set-logic ALL)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --sygus-out=status --lang=sygus2
(set-logic ALL)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --sygus-out=status --lang=sygus2 --no-check-synth-sol
(set-logic ALL)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --sygus-out=status --lang=sygus2 --no-check-synth-sol
(set-logic ALL)
-; EXPECT: unknown
+; EXPECT: fail
; COMMAND-LINE: --sygus-out=status --lang=sygus2 --no-check-synth-sol
(set-logic ALL)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --sygus-out=status --sygus-si=none --sygus-repair-const --lang=sygus2
(set-logic LIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --sygus-out=status
(set-logic LIA)
(synth-fun fr0 ((_v Int) (n Int) (x Int)) Int
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --sygus-qe-preproc --sygus-si=all --sygus-out=status
(set-logic LIA)
(synth-fun fr0 ((_v Int) (n Int) (x Int)) Int
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --sygus-out=status --lang=sygus2 --strings-exp
(set-logic S)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic ALL)
(synth-fun P ((x (Set Int))) Bool)
; COMMAND-LINE: --sygus-si=all --sygus-out=status
-; EXPECT: unsat
+; EXPECT: feasible
(set-logic UF)
; COMMAND-LINE: --sygus-si=all --sygus-out=status
-; EXPECT: unsat
+; EXPECT: feasible
(set-logic UF)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic SLIA)
(synth-fun P ((x String)) Bool
; COMMAND-LINE: --sygus-si=all --sygus-out=status
-; EXPECT: unsat
+; EXPECT: feasible
(set-logic UF)
; COMMAND-LINE: --sygus-si=all --sygus-out=status
-; EXPECT: unsat
+; EXPECT: feasible
(set-logic UF)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-inv-templ=post --sygus-out=status
(set-logic LIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status --no-sygus-pbe --sygus-si=none --sygus-grammar-cons=any-term
(set-logic ALL)
(synth-fun f ((x String) (y String)) Int)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic SLIA)
(synth-fun f ((x String)) String
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic SLIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic ALL)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic SLIA)
(synth-fun f ((firstname String) (lastname String)) String
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic SLIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic SLIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic SLIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic SLIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic SLIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status --decision=justification
(set-logic LIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic ALL)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic HO_ALL)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic LIA)
(
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic ALL)
(define-sort FP () (_ FloatingPoint 3 5))
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic DTSLIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status
(set-logic LIA)
(synth-fun f ((x Int)) Int
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status
(set-logic LIA)
(synth-fun f ((x Int)) Int
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status
(set-logic LIA)
(synth-fun f ((x Int)) Int
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic LIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status
(set-logic LIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status
(set-logic LIA)
(define-fun letf ((x Int) (y Int) (z Int)) Int (+ (+ y x) z))
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic LIA)
-; EXPECT: unsat\r
+; EXPECT: feasible\r
; COMMAND-LINE: --lang=sygus2 --sygus-fair=direct --sygus-out=status\r
(set-logic SLIA)\r
\r
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic LIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic LIA)
(synth-fun findSum ((y1 Int) (y2 Int)) Int ((Start Int) (BoolExpr Bool)) (
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-unif-pi=complete --sygus-out=status
(set-logic BV)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-repair-const --sygus-grammar-cons=any-const
(set-logic LIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic LIA)
(synth-fun f ((x Int) (y Int)) Int)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic BV)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status
(set-logic LIRA)
(define-fun
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
; Synthesize the maximum of 2 integers, but property has 4 variables (requires 2 passes)
(set-logic LIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status --fp-exp
(set-logic ALL)
(define-sort FP () (_ FloatingPoint 3 5))
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic LIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-enum=fast
(set-logic BV)
; COMMAND-LINE: --sygus-out=status --sygus-si=all
-; EXPECT: unsat
+; EXPECT: feasible
; This regression ensures that we are not too aggressive in filtering
; enumerated shapes in the pool.
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic LIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic BV)
(define-sort BV () (_ BitVec 8))
; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status --no-sygus-repair-const --sygus-arg-relevant
-; EXPECT: unsat
+; EXPECT: feasible
(set-logic LIA)
(synth-fun f ((x1 Int) (x2 Int) (x3 Int) (x4 Int) (x5 Int) (x6 Int) (x7 Int) (x8 Int) (x9 Int) (x10 Int)) Int)
; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status --no-sygus-add-const-grammar --sygus-arg-relevant
-; EXPECT: unsat
+; EXPECT: feasible
(set-logic LIA)
(synth-fun f ((x1 Int) (x2 Int) (x3 Int) (x4 Int) (x5 Int) (x6 Int) (x7 Int) (x8 Int) (x9 Int) (x10 Int)) Int)
; COMMAND-LINE: --sygus-out=status
-; EXPECT: unsat
+; EXPECT: feasible
(set-logic ALL)
(define-fun safe-mod ((x Int) (y Int)) Int (mod x (+ 1 (abs y))))
(synth-fun args_0_refinement_0
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-si=none --no-sygus-pbe
(set-logic LRA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-enum=fast
(set-logic ALL)
(synth-fun f ((x Int)) (Set Int))
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic ALL)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic UFLIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-enum=fast
(set-logic NIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-unif-pi=complete --cegis-sample=use
(set-logic LIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-unif-pi=complete --sygus-out=status
(set-logic LIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic LIA)
(synth-fun inv ((i Int) (l Int)) Bool
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status --nl-ext-tplanes
(set-logic NIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --sygus-out=status --lang=sygus2
(set-logic ALL)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status --decision=justification
(set-logic LIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status --no-sygus-pbe --sygus-si=none --sygus-grammar-cons=any-term --sygus-enum=smart
(set-logic ALL)
(synth-fun f ((x String) (y String)) Int)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic LIA)
(synth-fun inv ((i Int) (y Int) (l Int)) Bool
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-grammar-cons=any-term-concise --sygus-unif-pi=complete
(set-logic LIA)
-; EXPECT: unsat
+; EXPECT: feasible
; COMMAND-LINE: --lang=sygus2 --sygus-out=status --no-sygus-repair-const --decision=justification
(set-logic LIA)
ASSERT_THROW(d_solver.getSynthSolution(f), CVC5ApiException);
- d_solver.checkSynth();
+ cvc5::api::SynthResult sr = d_solver.checkSynth();
+ ASSERT_EQ(sr.hasSolution(), true);
ASSERT_NO_THROW(d_solver.getSynthSolution(f));
ASSERT_NO_THROW(d_solver.getSynthSolution(f));
d_solver.setOption("incremental", "true");
Term f = d_solver.synthFun("f", {}, d_solver.getBooleanSort());
- d_solver.checkSynth();
+ cvc5::api::SynthResult sr = d_solver.checkSynth();
+ ASSERT_EQ(sr.hasSolution(), true);
ASSERT_NO_THROW(d_solver.getSynthSolutions({f}));
- d_solver.checkSynthNext();
+ sr = d_solver.checkSynthNext();
+ ASSERT_EQ(sr.hasSolution(), true);
ASSERT_NO_THROW(d_solver.getSynthSolutions({f}));
}
ASSERT_FALSE(res_null.isUnknown());
}
+TEST_F(TestApiBlackSynthResult, hasSolution)
+{
+ d_solver.setOption("sygus", "true");
+ Term f = d_solver.synthFun("f", {}, d_solver.getBooleanSort());
+ Term boolTerm = d_solver.mkTrue();
+ d_solver.addSygusConstraint(boolTerm);
+ cvc5::api::SynthResult res = d_solver.checkSynth();
+ ASSERT_FALSE(res.isNull());
+ ASSERT_TRUE(res.hasSolution());
+ ASSERT_FALSE(res.hasNoSolution());
+ ASSERT_FALSE(res.isUnknown());
+}
+
+TEST_F(TestApiBlackSynthResult, hasNoSolution)
+{
+ // note that we never return synth result for which hasNoSolution is true
+ // currently
+ cvc5::api::SynthResult res_null;
+ ASSERT_FALSE(res_null.hasNoSolution());
+}
+
+TEST_F(TestApiBlackSynthResult, isUnknown)
+{
+ d_solver.setOption("sygus", "true");
+ Term f = d_solver.synthFun("f", {}, d_solver.getBooleanSort());
+ Term boolTerm = d_solver.mkFalse();
+ d_solver.addSygusConstraint(boolTerm);
+ cvc5::api::SynthResult res = d_solver.checkSynth();
+ // currently isUnknown, could also return hasNoSolution when support for
+ // infeasibility of sygus conjectures is added.
+ ASSERT_FALSE(res.isNull());
+ ASSERT_FALSE(res.hasSolution());
+ ASSERT_FALSE(res.hasNoSolution());
+ ASSERT_TRUE(res.isUnknown());
+}
+
} // namespace test
} // namespace cvc5
assertThrows(CVC5ApiException.class, () -> d_solver.getSynthSolution(f));
- d_solver.checkSynth();
+ SynthResult sr = d_solver.checkSynth();
+ assertEquals(sr.hasSolution(), true);
assertDoesNotThrow(() -> d_solver.getSynthSolution(f));
assertDoesNotThrow(() -> d_solver.getSynthSolution(f));
d_solver.setOption("incremental", "true");
Term f = d_solver.synthFun("f", new Term[] {}, d_solver.getBooleanSort());
- d_solver.checkSynth();
+ SynthResult sr = d_solver.checkSynth();
+ assertEquals(sr.hasSolution(), true);
assertDoesNotThrow(() -> d_solver.getSynthSolutions(new Term[] {f}));
- d_solver.checkSynthNext();
+ sr = d_solver.checkSynthNext();
+ assertEquals(sr.hasSolution(), true);
assertDoesNotThrow(() -> d_solver.getSynthSolutions(new Term[] {f}));
}
assertFalse(res_null.hasNoSolution());
assertFalse(res_null.isUnknown());
}
+
+ @Test void hasSolution()
+ {
+ d_solver.setOption("sygus", "true");
+ Term f = d_solver.synthFun("f", new Term[] {}, d_solver.getBooleanSort());
+ Term boolTerm = d_solver.mkTrue();
+ d_solver.addSygusConstraint(boolTerm);
+ SynthResult res = d_solver.checkSynth();
+ assertFalse(res.isNull());
+ assertTrue(res.hasSolution());
+ assertFalse(res.hasNoSolution());
+ assertFalse(res.isUnknown());
+ }
+
+ @Test void hasNoSolution()
+ {
+ SynthResult res_null = d_solver.getNullSynthResult();
+ assertFalse(res_null.hasSolution());
+ }
+
+ @Test void isUnknown()
+ {
+ d_solver.setOption("sygus", "true");
+ Term f = d_solver.synthFun("f", new Term[] {}, d_solver.getBooleanSort());
+ Term boolTerm = d_solver.mkTrue();
+ d_solver.addSygusConstraint(boolTerm);
+ SynthResult res = d_solver.checkSynth();
+ assertFalse(res.isNull());
+ assertTrue(res.hasSolution());
+ assertFalse(res.hasNoSolution());
+ assertFalse(res.isUnknown());
+ }
}
with pytest.raises(RuntimeError):
solver.getSynthSolution(f)
- solver.checkSynth()
+ res = solver.checkSynth()
+ assert res.hasSolution()
solver.getSynthSolution(f)
solver.getSynthSolution(f)
solver.setOption("incremental", "true")
f = solver.synthFun("f", [], solver.getBooleanSort())
- solver.checkSynth()
+ res = solver.checkSynth()
+ assert res.hasSolution()
solver.getSynthSolutions([f])
- solver.checkSynthNext()
+ res = solver.checkSynthNext()
+ assert res.hasSolution()
solver.getSynthSolutions([f])
def test_check_synth_next2(solver):
assert not res_null.hasSolution()
assert not res_null.hasNoSolution()
assert not res_null.isUnknown()
+
+def test_has_solution(solver):
+ solver.setOption("sygus", "true")
+ f = solver.synthFun("f", [], solver.getBooleanSort())
+ boolTerm = solver.mkBoolean(True)
+ solver.addSygusConstraint(boolTerm)
+ res = solver.checkSynth()
+ assert not res_null.isNull()
+ assert res_null.hasSolution()
+ assert not res_null.hasNoSolution()
+ assert not res_null.isUnknown()
+
+def test_has_no_solution(solver):
+ res_null = SynthResult(solver)
+ assert not res_null.hasNoSolution()
+
+def test_has_is_unknown(solver):
+ solver.setOption("sygus", "true")
+ f = solver.synthFun("f", [], solver.getBooleanSort())
+ boolTerm = solver.mkBoolean(False)
+ solver.addSygusConstraint(boolTerm)
+ res = solver.checkSynth()
+ assert not res_null.isNull()
+ assert not res_null.hasSolution()
+ assert not res_null.hasNoSolution()
+ assert res_null.isUnknown()
projects / cvc5.git / commitdiff