Allow for checking proposed solution

[eionblanc]

Develop a feature which can input a proposed model-lemma to a grammar and decide whether or not this proposition could have been the result of some model applied to the grammar's synthesized lemma.

This could be done by checking all possible models (mod equivalence from nested ite statements) to see if any generate the proposed solution when applied to the synthesized lemma.

[muraliadithya]

Let us do this on the cleanup branch rather than main (perhaps after resolving #10 so we are sure that things are working correctly). There are two components to this: (i) Checking if the given candidate can be generated from the grammar: the way to do this is to essentially 'parse' the given candidate according to the grammar and check if it can be produced. This is slightly nontrivial. (ii) Assuming it can be generated from the grammar, all we have to do is take the candidate (presumably provided as a string in SMT-Lib format) and make it the body of our 'evaluation' function (the boolean variables no longer make sense, as they won't be used anyway). The solver should then say 'sat' if it is a correct candidate, since it does satisfy the constraints. This is easy.

The more accurate version of (ii) that can be used even if we have quantified constraints and such is to collect the constraints, make a disjunction over them, negate that expression and give that as one big constraints. Now check if the solver says 'unsat'. This says that there is no way the given candidate can refute even one of the constraints, and is a better check. In our case all of our constraints are variable-free, and therefore it is sufficient to simply do the above suggestion.

[eionblanc]

Component (i) should be implementable via the Cocke-Younger-Kasami algorithm in polynomial time, but this requires converting the grammar to Chomsky normal form first (also polynomial). Instead, I will first try the naive solution of checking all possible rule applications (implementation could resemble the _post attribute computation in the cleanup branch) to see if it suffices in terms of runtime, since our grammars are finite.

[eionblanc]

Thanks to the lisplike module, this became much simpler than suggested in my earlier comment. This needs more testing, but I believe component (i) is complete via the is_admissible function in SyGuSGrammar. An example of use, when grammar is some SyGusGrammar: >>string = '(=> (member x (hbst y)) (and (<= (key x) (maxr x)) (<= (minr x) (key y))))' >>string_lisp = lisplike.parse(string) >>grammar.is_admissible(string_lisp) True

The return is currently just a bool, but could be extended to give the replacement rule tree certifying admissibility.

[muraliadithya]

That's great! It's good to have some component doing the job. We can always have two versions, a 'cheap' check that checks only if the proposed solution satisfies the constraints, and the 'expensive' check that involves checking membership in the grammar as well.

[eionblanc]

The core solution to (ii) is set-up, but I'm not sure the interface is yet as desired. Currently, solutions may be proposed (and run for satisfiability in stead of the synthesized function as the lemma "body") via the options arguments in sygus_to_smt. So, I think this ends up being rather inaccessible to the user through terminal (and maybe that's acceptable).

Here's an example from a notebook:

proposals = {
    'lemma': '(not (dlst nil))',
    'rswitch': '(1)',
}
options = {'proposed_solutions': proposals}
grammars = sygus_to_smt('data/out_sdlist-dlist-and-slist.sy', 'prop_test.smt2', options)
for grammar in grammars:
    name = grammar.sygus_grammar.get_name()
    proposal = options['proposed_solutions'][name]
    admissible = grammar.sygus_grammar.is_admissible(parse(proposal))
    print('proposal {} for {} is admissible: {}'.format(proposal,name,admissible))

The printed result is:

proposal (not (dlst nil)) for lemma is admissible: True
proposal (1) for rswitch is admissible: True

The program does not check for admissibility when replacing synthesized functions with proposed solutions (the line to do so is currently commented out) in order for the default to be the 'cheap' check Adithya mentioned above. So the user must run the 'expensive' check manually. Since the grammar is required for the 'expensive' check, this (manual check) occurs after running sygus_to_smt, which is a bit awkward.

N.B. In the above example, (1) was the proposal rather than 1 due to needing compatibility with lisplike.parse. The function currently doesn't handle strings without parentheses.