sygus « regress0 « regress « test - cvc5.git - CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

Mode	Name	Size
-rw-r--r--	Makefile	142	log plain
-rw-r--r--	Makefile.am	1792	log plain
-rw-r--r--	array_search_2.sy	561	log plain
-rw-r--r--	array_sum_2_5.sy	458	log plain
-rw-r--r--	clock-inc-tuple.sy	496	log plain
-rw-r--r--	commutative.sy	376	log plain
-rw-r--r--	const-var-test.sy	649	log plain
-rw-r--r--	constant.sy	401	log plain
-rw-r--r--	dt-no-syntax.sy	249	log plain
-rw-r--r--	dt-test-ns.sy	321	log plain
-rw-r--r--	dup-op.sy	252	log plain
-rw-r--r--	enum-test.sy	233	log plain
-rw-r--r--	hd-01-d1-prog.sy	575	log plain
-rw-r--r--	icfp_28_10.sy	1475	log plain
-rw-r--r--	inv-example.sy	576	log plain
-rw-r--r--	let-ringer.sy	434	log plain
-rw-r--r--	let-simp.sy	340	log plain
-rw-r--r--	list-head-x.sy	287	log plain
-rw-r--r--	max.smt2	3751	log plain
-rw-r--r--	max.sy	936	log plain
-rw-r--r--	max2-univ.sy	404	log plain
-rw-r--r--	multi-fun-polynomial2.sy	622	log plain
-rw-r--r--	nflat-fwd-3.sy	227	log plain
-rw-r--r--	nflat-fwd.sy	246	log plain
-rw-r--r--	no-flat-simp.sy	341	log plain
-rw-r--r--	no-mention.sy	259	log plain
-rw-r--r--	no-syntax-test-bool.sy	215	log plain
-rw-r--r--	no-syntax-test-no-si.sy	217	log plain
-rw-r--r--	no-syntax-test.sy	209	log plain
-rw-r--r--	parity-AIG-d0.sy	799	log plain
-rw-r--r--	sygus-dt.sy	475	log plain
-rw-r--r--	sygus-uf.sl	449	log plain
-rw-r--r--	tl-type.sy	244	log plain
-rw-r--r--	twolets1.sy	703	log plain
-rw-r--r--	twolets2-orig.sy	593	log plain
-rw-r--r--	uminus_one.sy	184	log plain
-rw-r--r--	unbdd_inv_gen_winf1.sy	1407	log plain