From c87ee73ad3d51c238700f236c18e425b80e8e7ac Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 5 May 2016 18:44:47 -0500 Subject: Compute term indices lazily in TermDb. Optimization for qcf to recognize irrelevant quantifiers based on irrelevant functions. Fix rewriter for prefix merges. Minor optimizations for LFSC. Work on --literal-matching. Updates to inst propagate, move instantiation filtering within qe. Enable sygus for string inputs. --- proofs/lfsc_checker/check.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'proofs/lfsc_checker/check.cpp') diff --git a/proofs/lfsc_checker/check.cpp b/proofs/lfsc_checker/check.cpp index c96791aeb..22e326cda 100644 --- a/proofs/lfsc_checker/check.cpp +++ b/proofs/lfsc_checker/check.cpp @@ -24,7 +24,7 @@ int colnum = 1; const char *filename = 0; FILE *curfile = 0; -//#define USE_HASH_MAPS +//#define USE_HASH_MAPS //AJR: deprecated symmap2 progs; std::vector< Expr* > ascHoles; -- cgit v1.2.3