smt - How to display specific unsat constraint, not whole core (Z3, Python) -

-

how can list specific constraint result unsat core? have lot of conditions , printing whole core doesn't print all. read can done assert_and_track , unsat_core commands. found examples don't works. experience this?

s.assert_and_track(a > b, 'p1') s.assert_and_track(b > c, 'p2') if s.check() == sat:   print('ok') else:   c = s.unsat_core   print(c) <- print core

so how print p1 or p2 (just true/false result) ? e.g. p2 = false, or can displayed in way displayed in print(c) mode - p1.

the easiest way achieve save map of labels constraints, examples can 

m = {} m['p1'] = (a > b) m['p2'] = (b > c) m['p3'] = (c > a)

so later can print core in terms of constraints, instance follows

core = s.unsat_core() e in core:     print(m[str(e)])

of course work if want print entries instead of of them.


Comments

Post a Comment

Popular posts from this blog

How to show in django cms breadcrumbs full path? -

-
need advice - how show in breadcrumbs whole path article or page? i've got code: {% ance in ancestors %} <li> {% if not forloop.last %} <a href="{{ ance.get_absolute_url }}">{{ ance.get_menu_title }}</a> {% else %} <span class="active">{{ ance.get_menu_title }}</span> {% endif %} </li> {% endfor %} but shows "home" , current page. how modify show whole path in breadcrumbs? i've found in file menu_tags.py code calls ancestors. @ least there class showbreadcrumbs: class showbreadcrumb(inclusiontag): """ shows breadcrumb node has same url current request - start level: after level should breadcrumb start? 0=home - template: template used render breadcrumb """ name = 'show_breadcrumb' template = 'menu/dummy.html' options = options( argument('start_level', default=0, require...
Read more

php - Invalid Cofiguration - yii\base\InvalidConfigException - Yii2 -

-
Image
i've installed yii2-user module/dektrium yii2-app-basic application command composer require "dektrium/yii2-user:0.9.*@dev" config/console.php return [ . . 'modules' => [ 'gii' => 'yii\gii\module', 'user' => [ 'class' => 'dektrium\user\module', ], ], . . ] config/web.php 'components' => [ . . /* 'user' => [ 'identityclass' => 'app\models\user', 'enableautologin' => true, ], */ 'modules' => [ 'user' => [ 'class' => 'dektrium\user\module', ], ], . . ] after that, run command $ php yii migrate/up --migrationpath=@vendor/dektrium/yii2-user/migrations updating database schema . but, when run http://localhost/mylawsuit/yii/web/index.php?r=u...
Read more

ruby on rails - npm error: tunneling socket could not be established, cause=connect ETIMEDOUT -

-
i have app uses rails framework , implements angularjs part of front end. i have pushed heroku , have heroku toolbelt installed, when try migrate db using "heroku run rake db:migrate" receive following error(s): installing core plugins heroku-cli-addons, heroku-apps, heroku-fork, heroku-git, heroku-local, heroku-run, heroku-status... error installing package. try running again gode_debug=info see more output. ! `run` not heroku command. ! perhaps meant `-h`, `2fa`, `auth`, `join`, `open`, `orgs`, `pg`, `ps` or `rake`. ! see `heroku help` list of available commands. i run command "gode_debug=info heroku run rake db:migrate" , receive error: npm err! darwin 14.5.0 npm err! argv "/users/christopher_pelnar/.heroku/node-v4.2.1-darwin-x64/bin/node" "/users/christopher_pelnar/.heroku/node-v4.2.1-darwin-x64/lib/node_modules/npm/cli.js" "install" "heroku-cli-addons" "heroku-apps" "heroku-fork...
Read more