This PR enables the dump tester, a parse-print-parse test for cvc5, on CI. It also includes some changes that reduce the number of regressions that fail with this tester.
check-examples: true
store-to-release: true
exclude_regress: 3-4
- run_regression_args: --tester base --tester model --tester synth --tester abduct
+ run_regression_args: --tester base --tester model --tester synth --tester abduct --tester dump
- name: macos:production
os: macos-11
check-examples: true
store-to-release: true
exclude_regress: 3-4
- run_regression_args: --tester base --tester model --tester synth --tester abduct
+ run_regression_args: --tester base --tester model --tester synth --tester abduct --tester dump
- name: ubuntu:production-clang
os: ubuntu-18.04
cache-key: productionclang
check-examples: true
exclude_regress: 3-4
- run_regression_args: --tester base --tester model --tester synth --tester abduct
+ run_regression_args: --tester base --tester model --tester synth --tester abduct --tester dump
- name: ubuntu:production-dbg
os: ubuntu-18.04
config: production --auto-download --assertions --tracing --unit-testing --java-bindings --editline
cache-key: dbg
exclude_regress: 3-4
- run_regression_args: --tester base --tester model --tester synth --tester abduct --tester proof
+ run_regression_args: --tester base --tester model --tester synth --tester abduct --tester proof --tester dump
- name: ubuntu:production-dbg-clang
os: ubuntu-latest
config: production --auto-download --assertions --tracing --cln --gpl
cache-key: dbgclang
exclude_regress: 3-4
- run_regression_args: --tester base --tester model --tester synth --tester abduct --tester unsat-core
+ run_regression_args: --tester base --tester model --tester synth --tester abduct --tester unsat-core --tester dump
name: ${{ matrix.name }}
runs-on: ${{ matrix.os }}
// commands. We invoke define-fun commands because they add function names
// to the symbol table.
if (solver->getOptionInfo("parse-only").boolValue()
+ && dynamic_cast<SetBenchmarkLogicCommand*>(cmd) == nullptr
&& dynamic_cast<DefineFunctionCommand*>(cmd) == nullptr
&& dynamic_cast<ResetCommand*>(cmd) == nullptr)
{
{
if (!solver->getOptionInfo("incremental").setByUser)
{
- cmd.reset(new SetOptionCommand("incremental", "true"));
- cmd->setMuted(true);
- pExecutor->doCommand(cmd);
+ solver->setOption("incremental", "true");
}
InteractiveShell shell(pExecutor->getSolver(),
pExecutor->getSymbolManager(),
{
if (!solver->getOptionInfo("incremental").setByUser)
{
- cmd.reset(new SetOptionCommand("incremental", "false"));
- cmd->setMuted(true);
- pExecutor->doCommand(cmd);
+ solver->setOption("incremental", "false");
}
ParserBuilder parserBuilder(
Parser::addOperator(api::APPLY_UF);
}
+ if (d_logic.isHigherOrder())
+ {
+ addOperator(api::HO_APPLY, "@");
+ }
+
if(d_logic.isTheoryEnabled(theory::THEORY_ARITH)) {
if(d_logic.areIntegersUsed()) {
defineType("Int", d_solver->getIntegerSort(), true, true);
ArrayStoreAll asa = n.getConst<ArrayStoreAll>();
out << "((as const ";
toStreamType(out, asa.getType());
- out << ") " << asa.getValue() << ")";
+ out << ") ";
+ toStreamCastToType(out,
+ asa.getValue(),
+ toDepth < 0 ? toDepth : toDepth - 1,
+ asa.getType().getArrayConstituentType());
+ out << ")";
break;
}
case kind::HO_APPLY:
if (!options::flattenHOChains())
{
+ out << smtKindString(k, d_variant) << ' ';
break;
}
// collapse "@" chains, i.e.
if (op.getIndices().empty())
{
// e.g. (tuple_project tuple)
- out << "project " << n[0] << ")";
+ out << "tuple_project " << n[0] << ")";
}
else
{
{
out << "(! ";
annot << ":no-pattern ";
- toStream(annot, nc, toDepth, nullptr);
+ toStream(annot, nc[0], toDepth, nullptr);
annot << ") ";
}
}
case kind::FORALL: return "forall";
case kind::EXISTS: return "exists";
+ // HO
+ case kind::HO_APPLY: return "@";
+
default:
; /* fall through */
}
TypeNode range,
Node formula) const
{
- out << "(define-fun " << id << " (";
+ out << "(define-fun " << cvc5::quoteSymbol(id) << " (";
if (!formals.empty())
{
vector<Node>::const_iterator i = formals.cbegin();
+; DISABLE-TESTER: dump
; REQUIRES: no-competition
-; EXPECT: (error "Parse Error: issue-4075.smt2:11.26: expecting number of repeats > 0
+; EXPECT: (error "Parse Error: issue-4075.smt2:12.26: expecting number of repeats > 0
; EXPECT:
; EXPECT: (simplify ((_ repeat 0) b))
; EXPECT: ^
+; DISABLE-TESTER: dump
; REQUIRES: no-competition
-; EXPECT: (error "Parse Error: issue-4130.smt2:10.39: expecting bit-width > 0
+; EXPECT: (error "Parse Error: issue-4130.smt2:11.39: expecting bit-width > 0
; EXPECT:
; EXPECT: (assert (and (= a (bv2nat ((_ int2bv 0) a)))))
; EXPECT: ^
; COMMAND-LINE: -o raw-benchmark
-; EXPECT: (set-option :incremental false)
; EXPECT: (set-logic ALL)
; EXPECT: (declare-datatypes ((nat 0)) (((succ (pred nat)) (zero))))
; EXPECT: (declare-fun x () nat)
; COMMAND-LINE: --bv-solver=bitblast
; EXPECT: unsat
-(set-logic QF_FP)
+(set-logic QF_FPLRA)
(declare-fun fpv5 () Float32)
(assert (fp.eq (fp.mul RTP fpv5 fpv5) ((_ to_fp 8 24) RTN 0.04)))
(check-sat)
+; DISABLE-TESTER: dump
; REQUIRES: no-competition
; SCRUBBER: grep -o "Symbol '->' not declared"
; EXPECT: Symbol '->' not declared
+; DISABLE-TESTER: dump
; EXPECT: sat
(set-logic ALL)
(set-info :status sat)
+; DISABLE-TESTER: dump
; REQUIRES: no-competition
; COMMAND-LINE: --input-agnuage
; ERROR-SCRUBBER: grep -o "--[a-zA-Z-]+"
+; DISABLE-TESTER: dump
; COMMAND-LINE: --help
; SCRUBBER: grep -o "usage: cvc5"
; EXPECT: usage: cvc5
+; DISABLE-TESTER: dump
; COMMAND-LINE: --print-success
; EXPECT: success
; EXPECT: success
+; DISABLE-TESTER: dump
; REQUIRES: no-competition
; EXPECT: sat
; EXPECT: not declared
; This regression ensures that we detect repeated set-logic commands even when
; --force-logic is used.
+; DISABLE-TESTER: dump
; COMMAND-LINE: --force-logic="QF_BV"
; SCRUBBER: grep -o "Only one set-logic is allowed."
; EXPECT: Only one set-logic is allowed.
+; DISABLE-TESTER: dump
; COMMAND-LINE: --produce-models
; EXPECT: sat
; EXPECT: (((f (as @a0 Foo)) 3))
+; DISABLE-TESTER: dump
; REQUIRES: no-competition
; COMMAND-LINE: --strict-parsing
; SCRUBBER: grep -o "Symbol 'div' not declared as a variable"
+; DISABLE-TESTER: dump
; REQUIRES: no-competition
; COMMAND-LINE: --strict-parsing
; SCRUBBER: grep -o "Symbol 'mod' not declared as a variable"
+; DISABLE-TESTER: dump
; REQUIRES: no-competition
; COMMAND-LINE: --strict-parsing
; SCRUBBER: grep -o "Symbol 'abs' not declared as a variable"
+; DISABLE-TESTER: dump
; REQUIRES: no-competition
; SCRUBBER: grep -o "Cannot name a term in a binder"
; EXPECT: Cannot name a term in a binder
+; DISABLE-TESTER: dump
; EXPECT: Symbol `sin' is shadowing a theory function symbol
; SCRUBBER: grep -o "Symbol \`sin' is shadowing a theory function symbol"
; EXIT: 1
+; DISABLE-TESTER: dump
; EXPECT: Symbol `exp' is shadowing a theory function symbol
; SCRUBBER: grep -o "Symbol \`exp' is shadowing a theory function symbol"
; EXIT: 1
+; DISABLE-TESTER: dump
; REQUIRES: no-competition
; EXPECT: Quantifier used in non-quantified logic
; SCRUBBER: grep -o "Quantifier used in non-quantified logic"
+; DISABLE-TESTER: dump
; COMMAND-LINE: -vvv --sygus-out=status --check-synth-sol --check-abducts
; ERROR-SCRUBBER: sed -e 's/.*//g'
; SCRUBBER: sed -e 's/.*//g'
+; DISABLE-TESTER: dump
; REQUIRES: no-competition
; COMMAND-LINE: --sygus-out=status --sygus-rec-fun --lang=sygus2
-; EXPECT-ERROR: (error "Parse Error: pLTL-sygus-syntax-err.sy:78.19: number of arguments does not match the constructor type
+; EXPECT-ERROR: (error "Parse Error: pLTL-sygus-syntax-err.sy:79.19: number of arguments does not match the constructor type
; EXPECT-ERROR:
; EXPECT-ERROR: (Op2 <O2> <F>)
; EXPECT-ERROR: ^
+; DISABLE-TESTER: dump
; REQUIRES: no-competition
-; EXPECT: (error "Parse Error: arrayinuf_error.smt2:8.21: Symbol 'Array' not declared as a type
+; EXPECT: (error "Parse Error: arrayinuf_error.smt2:9.21: Symbol 'Array' not declared as a type
; EXPECT:
; EXPECT: (declare-fun a (Array Bool Bool))
; EXPECT: ^
+; DISABLE-TESTER: dump
; REQUIRES: no-competition
; EXIT: 1
-; EXPECT: (error "Parse Error: errorcrash.smt2:6.29: Symbol 'Array' not declared as a type")
+; EXPECT: (error "Parse Error: errorcrash.smt2:7.29: Symbol 'Array' not declared as a type")
(set-logic QF_UF)
(declare-sort U 0)
(declare-fun x () (Array U U))
(set-info :smt-lib-version 2.6)
-(set-logic FP)
+(set-logic FPLRA)
(set-info :status unsat)
(declare-fun c_main_~E0~7 () (_ FloatingPoint 11 53))
(declare-fun c_main_~S~7 () (_ FloatingPoint 11 53))
if exit_status == STATUS_TIMEOUT:
exit_code = EXIT_SKIP if g_args.skip_timeout else EXIT_FAILURE
print("Timeout - Flags: {}".format(benchmark_info.command_line_args))
- elif output != benchmark_info.expected_output:
+ elif benchmark_info.compare_outputs and output != benchmark_info.expected_output:
exit_code = EXIT_FAILURE
print("not ok - Flags: {}".format(benchmark_info.command_line_args))
print()
print_colored(Color.YELLOW, error)
print("=" * 80)
print()
- elif error != benchmark_info.expected_error:
+ elif benchmark_info.compare_outputs and error != benchmark_info.expected_error:
exit_code = EXIT_FAILURE
print(
"not ok - Differences between expected and actual output on stderr - Flags: {}".format(
class DumpTester(Tester):
def applies(self, benchmark_info):
- return benchmark_info.expected_exit_status == EXIT_OK
+ return benchmark_info.benchmark_ext != ".p"
def run(self, benchmark_info):
ext_to_lang = {
".smt2": "smt2",
- ".p": "tptp",
".sy": "sygus",
}
"--lang={}".format(ext_to_lang[benchmark_info.benchmark_ext]),
],
benchmark_basename=tmpf.name,
- expected_output="",
+ expected_exit_status=0,
+ compare_outputs=False,
)
)
os.remove(tmpf.name)
"expected_error",
"expected_exit_status",
"command_line_args",
+ "compare_outputs",
],
)
expected_error=expected_error,
expected_exit_status=expected_exit_status,
command_line_args=all_args,
+ compare_outputs=True,
)
for tester_name, tester in g_testers.items():
if tester_name in testers and tester.applies(benchmark_info):
projects / cvc5.git / commitdiff